Contracts: always remove spurious do {... } while(0) loops

None of our contracts instrumentation should spuriously get confused by
these pseudo-loops (suggesting to users that they need to unwind those
loops). We already used to do this for non-DFCC code, now also apply it
with dynamic frames.

Author: tautschnig

src/goto-instrument/contracts/contracts.h

@@ -147,7 +147,7 @@ class code_contractst
     return loop_havoc_set;
   }
 
-  namespacet ns;
+  const namespacet ns;
 
 protected:
   goto_modelt &goto_model;

src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp

@@ -503,6 +503,10 @@ dfcc_cfg_infot::dfcc_cfg_infot(
 {
   dfcc_loop_nesting_grapht loop_nesting_graph;
   goto_programt &goto_program = goto_function.body;
+
+  // Clean up possible fake loops that are due to do { ... } while(0);
+  simplify_gotos(goto_program, ns);
+
   if(loop_contract_config.apply_loop_contracts)
   {
     messaget log(message_handler);

src/goto-instrument/contracts/utils.cpp

@@ -257,7 +257,7 @@ void insert_before_and_update_jumps(
   }
 }
 
-void simplify_gotos(goto_programt &goto_program, namespacet &ns)
+void simplify_gotos(goto_programt &goto_program, const namespacet &ns)
 {
   for(auto &instruction : goto_program.instructions)
   {
@@ -270,7 +270,7 @@ void simplify_gotos(goto_programt &goto_program, namespacet &ns)
 
 bool is_loop_free(
   const goto_programt &goto_program,
-  namespacet &ns,
+  const namespacet &ns,
   messaget &log)
 {
   // create cfg from instruction list

src/goto-instrument/contracts/utils.h

@@ -199,13 +199,13 @@ void insert_before_and_update_jumps(
 
 /// Turns goto instructions `IF cond GOTO label` where the condition
 /// statically simplifies to `false` into SKIP instructions.
-void simplify_gotos(goto_programt &goto_program, namespacet &ns);
+void simplify_gotos(goto_programt &goto_program, const namespacet &ns);
 
 /// Returns true iff the given program is loop-free,
 /// i.e. if each SCC of its CFG contains a single element.
 bool is_loop_free(
   const goto_programt &goto_program,
-  namespacet &ns,
+  const namespacet &ns,
   messaget &log);
 
 /// Returns an \ref irep_idt that essentially says that