CONTRACTS (DFCC) main class and loop for whole model transformation

Author: Remi Delmas

src/goto-instrument/Makefile

@@ -17,6 +17,18 @@ SRC = accelerate/accelerate.cpp \
       branch.cpp \
       call_sequences.cpp \
       contracts/contracts.cpp \
+      contracts/dfcc_utils.cpp \
+      contracts/dfcc_library.cpp \
+      contracts/dfcc_instrument.cpp \
+      contracts/dfcc_spec_functions.cpp \
+      contracts/dfcc_contract_handler.cpp \
+      contracts/dfcc_swap_and_wrap.cpp \
+      contracts/dfcc_is_fresh.cpp \
+      contracts/dfcc_is_freeable.cpp \
+      contracts/dfcc_dsl_contract_handler.cpp \
+      contracts/dfcc_dsl_contract_functions.cpp \
+      contracts/dfcc_dsl_wrapper_program.cpp \
+      contracts/dfcc.cpp \
       contracts/havoc_assigns_clause_targets.cpp \
       contracts/instrument_spec_assigns.cpp \
       contracts/memory_predicates.cpp \