Changes required by the new dynamic frame condition checking system

[remi-delmas-3000]

Making the new goto-instrument contracts system available to users (https://github.com/diffblue/cbmc/pull/) require adaptations to the proof build process.

Initially, we would like to allow using the existing build process, and use a new one by setting the USE_DFCC environment variable to 1 (DFCC is short for Dynamic Drame Condition Checking).

When USE_DFCC is set the new build steps should be:

• build and link project and proof sources as usual
• call goto-instrument with function pointer restrictions switches
• call goto-instrument with CPROVER library configuration flags (such as malloc failure modes or --string-abstraction), proof harness identifier, function contract replacement switches, function contract checking switches (and in the future, loop contracts switches);
• call goto-instrument with loop unrolling directives for both user-defined loops and loops found in the CPROVER library (will unroll any remaining loops not replaced by loop contracts, assigns clause instrumentation scales automatically)
• call cbmc with switches for checks, without --unwind 1. Removing the unwind bound is needed so that all loops introduced by dynamic frame condition checking can be dynamically unwound to completion during SymEx.