Skip to content

accessedOffsetInRangeCTimesLid and accessedOffsetInRangeCTimesGid invariant generation rules never trigger #23

Open
@jeroenk

Description

This is due to commit 68bc077, which causes GPUVerify to generate statements like assume v0 and assume !v0 instead of assume v0 && v0 and assume !v0 && !v0. This breaks the logic of GetILessThanC, which depends on && occurring at the root of the expression.

We should investigate whether the rules can simply be removed, because they have been superseded by access breaking, or whether we can make them less fragile.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions