CONTRACTS: Add dfcc_dsl_wrapper_programt class

The class generates a sequence of GOTO instruction from
a contract expressed in the DSL syntax.
The instructions either encode a checked call to the function
under verification (CHECK mode) or an abstraction derived from
the contract (REPLACE mode).

In CHECK mode, it generates GOTO instructions
that assume preconditions, snapshots history variables,
creates a write set instance, call the function under verification
asserts the postconditions, and returns the call's return value.

In REPLACE mode, it generates GOTO
instructions encoding the nondeterministic abstraction
defined by the contract: assert preconditions,
create and havoc assigns clause targets, create
a nondet return value for the call, nondeterministically free
frees clause targets, assume postconditions, return
a value that satisfies the post conditions.

These instructions are meant to be added to the
GOTO function that serves as a wrapper for the function
under verification or being replaced by the contract.

Author: Remi Delmas

src/goto-instrument/Makefile

@@ -24,6 +24,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_instrument.cpp \
       contracts/dynamic-frames/dfcc_spec_functions.cpp \
       contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp \
+      contracts/dynamic-frames/dfcc_dsl_wrapper_program.cpp \
       contracts/havoc_assigns_clause_targets.cpp \
       contracts/instrument_spec_assigns.cpp \
       contracts/memory_predicates.cpp \