Applying loop and/or function contracts transformations (without the dynamic frames method)

The program transformation takes the following parameters:

goto-instrument [--apply-loop-contracts] [--enforce-contract <function>] (--replace-call-with-contract <function>)* in.gb out.gb

Where:

--apply-loop-contracts is optional and specifies to apply loop contracts globally;
--enforce-contract <function> is optional and specifies that function must be checked against its contract.
--replace-call-with-contract <function> is optional and specifies that all calls to function must be replaced with its contract;

Applying the function contracts transformation (with the dynamic frames method)

The program transformation takes the following parameters:

goto-instrument --dfcc harness [--enforce-contract <function>[/<contract>]] (--replace-call-with-contract <function>[/<contract>])* in.gb out.gb

Where:

--dfcc harness specifies the proof harness (i.e. the entry point of the analysis);
--enforce-contract <function>[/<contract>] is optional and specifies that function must be checked against contract. When contract is not specfied, the contract is assumed to be carried by the function itself.
--replace-call-with-contract <function>[/<contract>] is optional and specifies that all calls to function must be replaced with contract. When contract is not specfied, the contract is assumed to be carried by the function itself.