cprover
|
Back to top Code Contracts Transformation Specification
The __CPROVER_obeys_pointer is defined as follows: if the predicate holds then function_pointer points to a function satisfying the contract passed as second argument. If the predicate does not hold, then nothing can be assumed of the function_pointer behaviour.
The instrumentation of __CPROVER_obeys_contract is supported by the class dfcc_obeys_contractt. In a GOTO program passed as argument, this class rewrites calls to:
into calls to the library function implementation:
One thing to notice is that the library implementation function takes the function_pointer argument by reference:
This function implements the __CPROVER_obeys_contract behaviour for all different contexts (contract checking vs replacement, requires vs ensures clause context, as described by the flags carried by the write set parameter).
In an assumption context, the predicate turns into a nondet assignment that makes function_pointer point to the contract function:
If the surrounding __CPROVER_assume statement enforces a true value for the predicate, then the function_pointer will effectively point to the contract function, which is known to satisfy its own specification.
If the surrounding __CPROVER_assume statement enforces a false value for the predicate, then nothing is enforced on the function_pointer (it could be invalid, be NULL, point to any other function, etc.).
In assertion contexts, the predicate turns into a pointer equality check:
In addition to rewriting calls, the dfcc_obeys_contractt class reports all contract functions discovered as second arguments of the predicates. This information is then used in method dfcct::wrap_discovered_function_pointer_contracts to replace all discovered contract functions by their actual contracts. That way, any call to a function pointer assumed or succesfully asserted to satisfy the contract will actually behave like the contract.
Prev | Next |
---|---|
Code Contracts Developer Documentation | Function Contracts Reminder |