CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Generating GOTO Functions From Contract Clauses

Back to top Code Contracts Transformation Specification

Translating Assigns Clauses to GOTO Functions

Let's consider a contract foo (with corresponding pure contract contract::foo) with a __CPROVER_assigns(A) clause.

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

We know the elements of A only depend on foo-parameters and global variables.

A new GOTO function with the following signature is generated:

void contract::foo::assigns(foo-parameters);

The body of the function generated from the elements of A as follows:

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.

void contract::foo::assigns(
// function parameters
foo-parameters,
// write set to populate with new targets
// write set against which to check itself for unwanted side effects
Runtime representation of a write set.

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:

Translating Frees Clauses to GOTO Functions

Let's consider a contract foo (with corresponding pure contract contract::foo) with a __CPROVER_frees(F) clause.

ret_t foo(foo-parameters) __CPROVER_frees(F);

We know the elements of F only depend on foo-parameters and global variables.

A new GOTO function with the following signature is generated:

void contract::foo::frees(foo-parameters);

The body of the function generated from the elements of F as follows:

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.

void contract::foo::frees(
// function parameters
foo-parameters,
// write set to populate with new targets
// write set against which to check itself for unwanted side effects

Prev Next
Program Transformation Overview Rewriting Declarative Assign and Frees Specification Functions