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

Declarations are printed as part of a symex trace, and come with both a
symbol being declared as well as an (unconstrained) initial value for
that symbol. The decision procedure must learn about the initial value
to include it in the model. Else, the trace value would just be question
marks.

Fixes: #6845

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