Merge pull request #7875 from esteffin/esteffin/fix-shadow-memory-trace

Fix shadow memory trace generation

Author: Enrico Steffinlongo

regression/cbmc-shadow-memory/trace1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --stop-on-fail --unwind 5
 ^EXIT=10$

src/goto-programs/remove_returns.cpp

@@ -17,8 +17,9 @@ Date:   September 2009
 #include <util/std_expr.h>
 #include <util/suffix.h>
 
-#include "goto_model.h"
+#include <goto-symex/shadow_memory.h>
 
+#include "goto_model.h"
 #include "remove_skip.h"
 
 #define RETURN_VALUE_SUFFIX "#return_value"
@@ -225,7 +226,10 @@ void remove_returnst::operator()(goto_functionst &goto_functions)
         findit != goto_functions.function_map.end(),
         "called function `" + id2string(function_id) +
           "' should have an entry in the function map");
-      return !findit->second.body_available();
+      return !findit->second.body_available() &&
+             function_id != CPROVER_PREFIX SHADOW_MEMORY_FIELD_DECL &&
+             function_id != CPROVER_PREFIX SHADOW_MEMORY_GET_FIELD &&
+             function_id != CPROVER_PREFIX SHADOW_MEMORY_SET_FIELD;
     };
 
     replace_returns(gf_entry.first, gf_entry.second);

src/goto-symex/shadow_memory.h

@@ -23,6 +23,7 @@ Author: Peter Schrammel
 #define SHADOW_MEMORY_LOCAL_SCOPE "_local"
 #define SHADOW_MEMORY_GET_FIELD "get_field"
 #define SHADOW_MEMORY_SET_FIELD "set_field"
+#define SHADOW_MEMORY_SYMBOL_PREFIX "__SM"
 
 class code_function_callt;
 class abstract_goto_modelt;

src/goto-symex/symex_assign.cpp

@@ -228,7 +228,9 @@ void symex_assignt::assign_non_struct_symbol(
   state.record_events.pop();
 
   auto current_assignment_type =
-    ns.lookup(l2_lhs.get_object_name()).is_auxiliary
+    ns.lookup(l2_lhs.get_object_name()).is_auxiliary &&
+        id2string(l2_lhs.get_object_name()).find(SHADOW_MEMORY_SYMBOL_PREFIX) !=
+          std::string::npos
       ? symex_targett::assignment_typet::HIDDEN
       : assignment_type;