Merge pull request #6875 from tautschnig/bugfixes/6845-part-2-decl

Goto-symex: record value-at-declaration in the back-end

Author: tautschnig

regression/cbmc/atomic_section_seq1/test.desc

@@ -1,8 +1,11 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
+This test involves empty structs, which the SMT2 back-end does not currently
+support.

regression/cbmc/trace-values/trace-values.c

@@ -16,6 +16,7 @@ int main()
   int *q=&my_nested[1].f;
   int *null=0;
   int *junk;
+  struct S s;
 
   global_var=1;
   static_var=2;
@@ -34,6 +35,9 @@ int main()
   // assign entire struct
   my_nested[1]=my_nested[0];
 
+  // struct member
+  s.f = 42;
+
   // get a trace
   __CPROVER_assert(0, "");
 }

regression/cbmc/trace-values/trace-values.desc

@@ -3,6 +3,7 @@ trace-values.c
 --trace
 ^EXIT=10$
 ^SIGNAL=0$
+^  s=\{ \.f=-?\d+, \.array=\{ -?\d+, -?\d+, -?\d+ \} \} \(\{ [01 ]+, \{ [01 ]+, [01 ]+, [01 ]+ \} \}\)$
 ^  global_var=1 .*$
 ^  static_var=2 .*$
 ^  local_var=3 .*$
@@ -12,6 +13,7 @@ trace-values.c
 ^  dynamic_object1\[1.*\]=8 .*$
 ^  my_nested\[1.*\](=\{ )?.f=0[ ,]
 ^  my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
+^  s\.f=42 \([0 ]+ 00101010\)$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

src/goto-symex/symex_target_equation.cpp

@@ -389,6 +389,8 @@ void symex_target_equationt::convert_decls(
       // The result is not used, these have no impact on
       // the satisfiability of the formula.
       decision_procedure.handle(step.cond_expr);
+      decision_procedure.handle(
+        equal_exprt{step.ssa_full_lhs, step.ssa_full_lhs});
       step.converted = true;
       with_solver_hardness(
         decision_procedure, hardness_register_ssa(step_index, step));