CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Program Transformation Overview

Back to top Code Contracts Transformation Specification

These are the main parameter of the program transformation:

  • harness_id specifies the identifier of the proof harness;
  • (f_top,c_top) an optional pair and specifies that the function f_top must be checked against the contract carried by function c_top, by the pure contract contract::c_top.
  • (f,c) a possibly empty set of pairs where each f must be replaced with the contract carried by function c, i.e. by the pure contract contract::c.

The program transformation steps are applied as follows:

  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;

Prev Next
Function Contracts Reminder Generating GOTO Functions From Contract Clauses