Move assignment to init-flag to harness-function

Now that we do not presuppose cprove_initialize the assignment has to be
somewhere.

Author: Petr Bauch

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -170,28 +170,12 @@ void memory_snapshot_harness_generatort::add_init_section(
   goto_modelt &goto_model) const
 {
   goto_functionst &goto_functions = goto_model.goto_functions;
-  symbol_tablet &symbol_table = goto_model.symbol_table;
 
   goto_functiont &goto_function =
     goto_functions.function_map[entry_function_name];
-  const symbolt &function_symbol = symbol_table.lookup_ref(entry_function_name);
 
   goto_programt &goto_program = goto_function.body;
 
-  // introduce a symbol for a Boolean variable to indicate the point at which
-  // the function initialisation is completed
-  symbolt &func_init_done_symbol = get_fresh_aux_symbol(
-    bool_typet(),
-    id2string(entry_function_name),
-    "func_init_done",
-    function_symbol.location,
-    function_symbol.mode,
-    symbol_table);
-  func_init_done_symbol.is_static_lifetime = true;
-  func_init_done_symbol.value = false_exprt();
-
-  const symbol_exprt func_init_done_var = func_init_done_symbol.symbol_expr();
-
   const goto_programt::const_targett start_it =
     goto_program.instructions.begin();
 
@@ -235,6 +219,9 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
       recursive_initialization.initialize(symbol.symbol_expr(), 0, {}, code);
     }
   }
+
+  code.add(code_assignt{func_init_done_var, false_exprt{}});
+
   return code;
 }
 
@@ -337,6 +324,19 @@ void memory_snapshot_harness_generatort::generate(
   const symbolt *called_function_symbol =
     symbol_table.lookup(entry_function_name);
 
+  // introduce a symbol for a Boolean variable to indicate the point at which
+  // the function initialisation is completed
+  auto &func_init_done_symbol = get_fresh_aux_symbol(
+    bool_typet(),
+    id2string(entry_function_name),
+    "func_init_done",
+    source_locationt::nil(),
+    called_function_symbol->mode,
+    symbol_table);
+  func_init_done_symbol.is_static_lifetime = true;
+  func_init_done_symbol.value = false_exprt();
+  func_init_done_var = func_init_done_symbol.symbol_expr();
+
   add_init_section(goto_model);
 
   code_blockt harness_function_body =

src/goto-harness/memory_snapshot_harness_generator.h

@@ -159,6 +159,8 @@ class memory_snapshot_harness_generatort : public goto_harness_generatort
   optionalt<unsigned> line_number;
   optionalt<goto_programt::const_targett> start_instruction;
 
+  symbol_exprt func_init_done_var;
+
   message_handlert &message_handler;
 };