Create SSA-level 2 names for individual fields

During symex, a declaration introduces non-deterministic values for the
declared symbol by creating a fresh L2 name without assigning any value
to it. With field-sensitive SSA, the same must be done for each field
(just like we already did the inverse for objects going out of scope via
a DEAD instruction).

Author: tautschnig

regression/cbmc/struct14/main.c

@@ -0,0 +1,14 @@
+struct S
+{
+  int x;
+};
+
+int main(int argc, char *argv[])
+{
+  struct S s;
+
+  if(argc > 3)
+    s.x = 42;
+
+  __CPROVER_assert(s.x == 42, "should fail");
+}

regression/cbmc/struct14/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+With field-sensitive SSA encoding we need to make sure that each struct member
+is treated as non-deterministic unless initialised.

src/goto-symex/symex_decl.cpp

@@ -67,6 +67,21 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   std::size_t generation = state.increase_generation(l1_identifier, ssa);
   CHECK_RETURN(generation == 1);
 
+  const exprt fields = state.field_sensitivity.get_fields(ns, state, ssa);
+  if(fields != ssa)
+  {
+    std::set<symbol_exprt> fields_set;
+    find_symbols(fields, fields_set);
+
+    for(const auto &l1_symbol : fields_set)
+    {
+      ssa_exprt field_ssa = to_ssa_expr(l1_symbol);
+      std::size_t field_generation =
+        state.increase_generation(l1_symbol.get_identifier(), field_ssa);
+      CHECK_RETURN(field_generation == 1);
+    }
+  }
+
   const bool record_events=state.record_events;
   state.record_events=false;
   exprt expr_l2 = state.rename(std::move(ssa), ns).get();