-
Notifications
You must be signed in to change notification settings - Fork 277
Open
Labels
Code ContractsFunction and loop contractsFunction and loop contractsawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersenhancement
Description
Similar to how __CPROVER_assert(bool cond, char *msg)
accepts a string that shows up in the terminal output,
we could modify the front end to allow users to name ensures and requires clauses in function contracts with an optional string. For example,
int foo(int *arr, size_t size)
__CPROVER_requires(size > 0 , "some text")
__CPROVER_ensures(__CPROVER_return_value == 1 , "some text")
{
}
Metadata
Metadata
Assignees
Labels
Code ContractsFunction and loop contractsFunction and loop contractsawsBugs or features of importance to AWS CBMC usersBugs or features of importance to AWS CBMC usersenhancement