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)
// preconditions
__CPROVER_requires(R)
 
// postconditions
__CPROVER_ensures(E)
 
// frame conditions
__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.

Prev	Next
Code Contracts Transformation Specification	Program Transformation Overview