Clean-up harnesses in testing symbol init-ability

also add mode to memory-snapshot.

Author: petr-bauch

src/goto-harness/function_call_harness_generator.cpp

@@ -11,7 +11,6 @@ Author: Diffblue Ltd.
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
 #include <util/exception_utils.h>
-#include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
@@ -213,10 +212,7 @@ void function_call_harness_generatort::implt::generate_nondet_globals(
     for(const auto &symbol_table_entry : *symbol_table)
     {
       const auto &symbol = symbol_table_entry.second;
-      if(
-        symbol.is_static_lifetime && symbol.is_lvalue &&
-        symbol.type.id() != ID_code &&
-        !has_prefix(id2string(symbol.name), CPROVER_PREFIX))
+      if(recursive_initialization->is_initialization_allowed(symbol))
       {
         globals.push_back(symbol.symbol_expr());
       }

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -231,7 +231,7 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
   for(auto pair : snapshot)
   {
     const auto name = id2string(pair.first);
-    if(name.find(CPROVER_PREFIX) != 0)
+    if(!has_prefix(name, CPROVER_PREFIX))
       ordered_snapshot_symbols.push_back(pair);
   }
 
@@ -249,7 +249,22 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
                pointer_depth(right.second.symbol_expr().type());
     });
 
-  code_blockt code;
+  code_blockt code{};
+
+  // add initialization for existing globals
+  for(const auto &pair : goto_model.symbol_table)
+  {
+    const auto &global_symbol = pair.second;
+    if(
+      global_symbol.is_static_lifetime && global_symbol.is_lvalue &&
+      global_symbol.type.id() != ID_code)
+    {
+      auto symeexr = global_symbol.symbol_expr();
+      if(symeexr.type() == global_symbol.value.type())
+        code.add(code_assignt{symeexr, global_symbol.value});
+    }
+  }
+
   for(const auto &pair : ordered_snapshot_symbols)
   {
     const symbolt &snapshot_symbol = pair.second;
@@ -374,6 +389,7 @@ void memory_snapshot_harness_generatort::generate(
 
   const symbolt *called_function_symbol =
     symbol_table.lookup(entry_location.function_name);
+  recursive_initialization_config.mode = called_function_symbol->mode;
 
   // introduce a symbol for a Boolean variable to indicate the point at which
   // the function initialisation is completed

src/goto-harness/recursive_initialization.h

@@ -16,6 +16,7 @@ Author: Diffblue Ltd.
 #include <util/expr.h>
 #include <util/message.h>
 #include <util/optional.h>
+#include <util/prefix.h>
 #include <util/std_types.h>
 
 #include "function_harness_generator_options.h"
@@ -71,6 +72,14 @@ class recursive_initializationt
     const recursion_sett &known_tags,
     code_blockt &body);
 
+  bool is_initialization_allowed(const symbolt &symbol)
+  {
+    return (
+      symbol.is_static_lifetime && symbol.is_lvalue &&
+      symbol.type.id() != ID_code &&
+      !has_prefix(id2string(symbol.name), CPROVER_PREFIX));
+  }
+
 private:
   const recursive_initialization_configt initialization_config;
   goto_modelt &goto_model;