Back to top Code Contracts Transformation Specification
The user documentation for function contracts is available at Function Contracts, but we briefly remind the developer of the structure of a contract below.
A contract is defined by adding one or more clauses to a function declaration or definition:
ret_t foo(parameters)
__CPROVER_ensures(E)
__CPROVER_assigns(A)
__CPROVER_frees(F)
;
- A __CPROVER_requires clause (Requires and Ensures Clauses) specifies a precondition as boolean expression R that may only depend on program globals, function parameters, memory predicates, function pointer predicates and deterministic, side effect-free function calls;
- A __CPROVER_ensures clause (Requires and Ensures Clauses) specifies a postcondition as boolean expression E that may only depend on program globals, function parameters, memory predicates, function pointer predicates, deterministic, side effect-free function calls, history variables, and the special variable __CPROVER_return_value;
- A __CPROVER_assigns clause (Assigns Clauses) specifies a set A of memory locations that may be assigned to by any function satisfying the contract;
- A __CPROVER_frees clause (Frees Clauses) specifies a set F of pointers that may be freed by any function satisfying the contract.
For each such function foo carrying contract clauses, the ansi-c front-end of CBMC creates a dedicated function symbol named contract::foo in the symbol table, with the same signature as foo, and attaches the contract clauses to that new symbol. We call contract::foo the pure contract associated with the function foo.