Symex trace: show implicit value associated with composite declarations

src/goto-symex/symex_decl.cpp

@@ -54,10 +54,10 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   target.decl(
     state.guard.as_expr(),
     ssa,
+    state.field_sensitivity.apply(ns, state, ssa, false),
     state.source,
-    hidden?
-      symex_targett::assignment_typet::HIDDEN:
-      symex_targett::assignment_typet::STATE);
+    hidden ? symex_targett::assignment_typet::HIDDEN
+           : symex_targett::assignment_typet::STATE);
 
   if(path_storage.dirty(ssa.get_object_name()) && state.atomic_section_id == 0)
     target.shared_write(

src/goto-symex/symex_target.h

@@ -127,15 +127,17 @@ class symex_targett
   /// Declare a fresh variable. The `cond_expr` is _lhs==lhs_.
   /// \param guard: Precondition for a declaration of this variable
   /// \param ssa_lhs: Variable to be declared, must be symbol (and not nil)
+  /// \param initializer: Initial value
   /// \param source: Pointer to location in the input GOTO program of this
   ///  declaration
   /// \param assignment_type: To distinguish between different types of
   ///  assignments (some may be hidden for the further analysis)
   virtual void decl(
     const exprt &guard,
     const ssa_exprt &ssa_lhs,
+    const exprt &initializer,
     const sourcet &source,
-    assignment_typet assignment_type)=0;
+    assignment_typet assignment_type) = 0;
 
   /// Remove a variable from the scope.
   /// \param guard: Precondition for removal of this variable

src/goto-symex/symex_target_equation.cpp

@@ -128,6 +128,7 @@ void symex_target_equationt::assignment(
 void symex_target_equationt::decl(
   const exprt &guard,
   const ssa_exprt &ssa_lhs,
+  const exprt &initializer,
   const sourcet &source,
   assignment_typet assignment_type)
 {
@@ -138,7 +139,7 @@ void symex_target_equationt::decl(
 
   SSA_step.guard=guard;
   SSA_step.ssa_lhs=ssa_lhs;
-  SSA_step.ssa_full_lhs=ssa_lhs;
+  SSA_step.ssa_full_lhs = initializer;
   SSA_step.original_full_lhs=ssa_lhs.get_original_expr();
   SSA_step.hidden=(assignment_type!=assignment_typet::STATE);
 

src/goto-symex/symex_target_equation.h

@@ -73,6 +73,7 @@ class symex_target_equationt:public symex_targett
   virtual void decl(
     const exprt &guard,
     const ssa_exprt &ssa_lhs,
+    const exprt &initializer,
     const sourcet &source,
     assignment_typet assignment_type);