Skip to content

Cprover should have an __enum_in_range primitive #5473

Closed
@danielsn

Description

@danielsn

It is currently difficult to use the --enum-range-check option, because it is hard to ensure in a harness that an enum is within range. IF there was a
__CPROVER_enum_is_in_range(e) primitive, we could use it like
__CPROVER_assume(__CPROVER_enum_is_in_range(e))
and
assert(__CPROVER_enum_is_in_range(e))

Metadata

Metadata

Assignees

No one assigned

    Labels

    awsBugs or features of importance to AWS CBMC usersnew feature

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions