CBMC
|
Back to top Code Contracts Transformation Specification
The first operation one can do with contracts is to check if a function satisfies a contract.
Let us consider a contract c
, a function foo
and a proof harness main
.
In order to check the contract c
against foo
in the context set up by the harness main
, we apply a swap-and-wrap transformation to the function foo
:
The swapping step consists in creating a fresh function foo_swapped
with the same interface as foo
and swapping the body of foo
into foo_swapped
, while instrumenting it for frame condition checking against A and F.
The wrapping step consists in creating a new body for foo
where the swapped function gets called between precondition and postcondition checking instructions generated from the contract:
After the swap-and-wrap transformation is applied, the main
function calls the contract-checking wrapper. Analysing this model with CBMC will effectively check that the initial foo
(now foo_swapped
), under the assumption that the contract preconditions hold, satisfies the postconditions and the frame conditions of the contract.
If the function to be checked is potentially recursive, we generate the wrapper function body such that the first call trigger the contract checking, and any subsequent call triggers the contract replacement logic as described in Replacing a Function by a Contract :
Prev | Next |
---|---|
Proof Harness Intrumentation | Replacing a Function by a Contract |