Merge pull request #4964 from hannes-steffenhagen-diffblue/fix/trace-decl-initializers

Symex trace: show implicit value associated with composite declarations

Author: hannes-steffenhagen-diffblue

regression/cbmc/field-sensitivity-trace-wrong-counterexample-1/test.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+struct SomeStruct
+{
+  int x;
+};
+
+int main(void)
+{
+  struct SomeStruct x;
+  // this should cause
+  // visible initialization of
+  // x to value other than 0
+  // if assertion fails
+  assert(x.x == 0);
+}

regression/cbmc/field-sensitivity-trace-wrong-counterexample-1/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+x=\{ \.x=0 \}
+^warning: ignoring
+--
+This tests for the counterexample shown in the trace having sensible values.
+In this case, we are asserting that x.x == 0, so x.x should have a value other
+than 0 if the assertion fails.

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);