Code Contracts Software Architecture

Back to Code Contracts Developer Documentation

Architecture Overview

The code implementing Code Contracts Transformation Specification is found in Dynamic Frame Condition Checking (DFCC)

We go over each class and explain how it works in relation to others.

The dfcct class is the main entry point into the transformation.

The method dfcct::transform_goto_model first separates the functions of the goto model in different groups (functions to instrument, pure contract symbols from which to generate code, functions to check against contracts, functions to replace with contracts) and applies the transformation to the whole goto model, by scheduling the translation passes described in Code Contracts Transformation Specification :

1. Generating GOTO Functions From Contract Clauses is applied to all contracts to check or replace;
2. Dynamic Frame Condition Checking is applied to all library or user-defined goto functions;
3. Proof Harness Intrumentation is applied to the harness function;
4. Checking a Contract Against a Function is applied to the function to be checked against a contract;
5. Replacing a Function by a Contract is applied to each function to be replaced by a contract;

Each of these translation passes is implemented in a specific class:

Class	Specification
dfcc_instrumentt	Implements Dynamic Frame Condition Checking for goto_functiont, goto_programt, or subsequences of instructions of goto_programt
dfcc_is_fresht	Implements Rewriting Calls to the __CPROVER_is_fresh Predicate
dfcc_pointer_in_ranget	Implements Rewriting Calls to the __CPROVER_pointer_in_range_dfcc Predicate
dfcc_pointer_equalst	Implements Rewriting Calls to the __CPROVER_pointer_equals Predicate
dfcc_lift_memory_predicatest	Implements Rewriting User-Defined Memory Predicates
dfcc_is_freeablet	Implements Rewriting Calls to __CPROVER_is_freeable and __CPROVER_was_freed Predicates
dfcc_obeys_contractt	Implements Rewriting Calls to the __CPROVER_obeys_contract Predicate
dfcc_spec_functionst	Implements Rewriting Declarative Assign and Frees Specification Functions
dfcc_wrapper_programt	Implements Checking a Contract Against a Function for contracts
	Implements Replacing a Function by a Contract for contracts
dfcc_contract_handlert	Implements Generating GOTO Functions From Contract Clauses for contracts
	Implements the interface dfcc_contract_handlert for contract by delegating operations to dfcc_wrapper_programt
dfcc_swap_and_wrapt	Implements Checking a Contract Against a Function by delegating basic operations to dfcc_contract_handlert
	Implements Replacing a Function by a Contract by delegating basic operations to dfcc_contract_handlert
	Implements Checking a Contract Against a Recursive Function by delegating basic operations to dfcc_contract_handlert

The following classes contain utility methods:

• dfcc_utilst : Provides basic utility methods to the other classes such as locating a function symbol, adding a parameter to a function symbol, cloning or renaming a function symbol, creating fresh symbols, inlining a function body, etc.
• dfcc_libraryt : Provides a C++ interface to access C library functions defined in cprover_contracts.c. Using this class it is possible to load the library symbols and post-process them with loop unrolling or inlining, etc.