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:
- Generating GOTO Functions From Contract Clauses is applied to all contracts to check or replace;
- Dynamic Frame Condition Checking is applied to all library or user-defined goto functions;
- Proof Harness Intrumentation is applied to the harness function;
- Checking a Contract Against a Function is applied to the function to be checked against a contract;
- Replacing a Function by a Contract is applied to each function to be replaced by a contract;