Make is_initialization_allowed static and change init conditions.

Author: NlightNFotis

src/goto-harness/function_call_harness_generator.cpp

@@ -281,7 +281,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(recursive_initialization->is_initialization_allowed(symbol))
+      if(recursive_initializationt::is_initialization_allowed(symbol))
       {
         globals.push_back(symbol.symbol_expr());
       }

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -248,9 +248,7 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_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)
+    if(recursive_initializationt::is_initialization_allowed(global_symbol))
     {
       auto symeexr = global_symbol.symbol_expr();
       if(symeexr.type() == global_symbol.value.type())
@@ -272,7 +270,8 @@ code_blockt memory_snapshot_harness_generatort::add_assignments_to_globals(
         ? fresh_symbol_copy(snapshot_symbol, symbol_table)
         : snapshot_symbol;
 
-    if(!fresh_or_snapshot_symbol.is_static_lifetime)
+    if(!recursive_initializationt::is_initialization_allowed(
+         fresh_or_snapshot_symbol))
       continue;
 
     if(variables_to_havoc.count(fresh_or_snapshot_symbol.base_name) == 0)

src/goto-harness/recursive_initialization.h

@@ -103,12 +103,14 @@ class recursive_initializationt
   /// \return the symbol expression for the `free` function
   symbol_exprt get_free_function();
 
-  bool is_initialization_allowed(const symbolt &symbol)
+  static bool is_initialization_allowed(const symbolt &symbol)
   {
+    auto const symbol_name = id2string(symbol.name);
     return (
       symbol.is_static_lifetime && symbol.is_lvalue &&
-      symbol.type.id() != ID_code &&
-      !has_prefix(id2string(symbol.name), CPROVER_PREFIX));
+      !symbol.type.get_bool(ID_C_constant) && symbol.type.id() != ID_code &&
+      !has_prefix(symbol_name, CPROVER_PREFIX) &&
+      !has_prefix(symbol_name, GOTO_HARNESS_PREFIX));
   }
 
   bool needs_freeing(const exprt &expr) const;