CONTRACTS: Add dfcc_dsl_contract_functionst class.

The class allows to translate the assigns clause
(or frees clause) of a contract expressed in DSL style
into GOTO a function describing the same set of targets
as the clause.

It also allows to generate a havoc function from an
assigns clause, that havocs the targets described by
the clause in a type-directed way.

Author: Remi Delmas

src/goto-instrument/Makefile

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