Skip to content

What is the proper annotation for ranges in function contracts #5966

@feliperodri

Description

@feliperodri

CBMC version: 5.26.0
Operating system: macOS Mojave
Exact command line resulting in the issue: N/A.
What behaviour did you expect: N/A.
What happened instead: N/A.

Currently, we support the specification of array ranges in code contracts using the syntax [lower .. upper]. However, this requires changes in the parser. @hannes-steffenhagen-diffblue suggested here a different approach:

I'm quite worried about the proliferation of nonstandard extensions. We're getting into a situation where we have to support gcc extensions, clang extensions, visual studio extensions on top of our own modifications to the language...
This could've been done without any parser changes at the relatively small cost of a less cute syntax, e.g. __CPROVER_array_range(array, lower, upper) or something like that. Looks bad, but less problematic syntactically.

Which one should we adopt?

Metadata

Metadata

Assignees

Labels

Code ContractsFunction and loop contractsMore info neededawsBugs or features of importance to AWS CBMC users

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions