Show shadow memory assignments in trace

Author: peterschrammel

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

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

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;