Merge pull request #8459 from tautschnig/contracts-remove-do-while-0

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

Author: tautschnig

regression/contracts-dfcc/invar_assigns_empty/test.desc

@@ -6,7 +6,6 @@ main.c
 ^\[main.loop_assigns.\d+\] line 5 Check assigns clause inclusion for loop .*: SUCCESS$
 ^\[main.loop_invariant_base.\d+\] line 5 Check invariant before entry for loop .*: SUCCESS$
 ^\[main.loop_invariant_step.\d+\] line 5 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 5 Check step was unwound for loop .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

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