CBMC
|
Back to top Code Contracts Transformation Specification
Let's consider a contract foo
(with corresponding pure contract contract::foo
) with a __CPROVER_assigns(A)
clause.
We know the elements of A only depend on foo-parameters
and global variables.
A new GOTO function with the following signature is generated:
The body of the function generated from the elements of A as follows:
cond: target
where the target is an lvalue expression: has_ptr_type(target)
returns true if the target has a pointer-type;cond: f(parameters)
, where f
is a void-typed function: Remark: The condition expressions needs to be goto_converted during translation since they come directly from the front-end and are allowed to contain function calls.
The rewriting pass Rewriting Assigns Clause Functions is applied to transform the function into a function that accepts two write set parameters: The first one is the write set that gets populated with assignable locations specified by the function, the second is a write set that is used by the function to check its side effects.
The rewriting step Generating Havoc Functions from Assigns Clause Functions is also applied to the function in order to generate a havoc function that can be used to model contract replacement:
Let's consider a contract foo
(with corresponding pure contract contract::foo
) with a __CPROVER_frees(F)
clause.
We know the elements of F only depend on foo-parameters
and global variables.
A new GOTO function with the following signature is generated:
The body of the function generated from the elements of F as follows:
cond: expr
where expr
is a pointer-typed expression: cond: f(params)
where f
is a void-typed function: Remark: The condition expressions needs to be goto_converted during translation since they come directly from the front-end and are allowed to contain function calls.
The resulting function is declarative, in the sense that it describes the contents of the frees clause but does not have any runtime effects.
The rewriting pass Rewriting Frees Clause Functions is applied to transform the function into a function that accepts two write set parameters: The first one is the write set that gets populated with freeable pointers specified by the function, the second is a write set that is used by the function to check its side effects.
Prev | Next |
---|---|
Program Transformation Overview | Rewriting Declarative Assign and Frees Specification Functions |