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;

Prev	Next
Function Contracts Reminder	Generating GOTO Functions From Contract Clauses