CONTRACTS: Add class dfcct (main class).

The class receives the proof harness function,
the map of functions and contracts to check
and the map of functions to replace with contracts.
It instruments the proof harness,  performs
swap-and-wrap operations for each of the checked
and replaced functions. It then instruments all
other functions for DFCC.

Author: Remi Delmas

src/goto-instrument/Makefile

@@ -27,6 +27,7 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_dsl_wrapper_program.cpp \
       contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp \
       contracts/dynamic-frames/dfcc_swap_and_wrap.cpp \
+      contracts/dynamic-frames/dfcc.cpp \
       contracts/havoc_assigns_clause_targets.cpp \
       contracts/instrument_spec_assigns.cpp \
       contracts/memory_predicates.cpp \