Merge pull request #4545 from tautschnig/uninitialised-struct-fix

Create SSA-level 2 names for individual fields

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

@@ -64,8 +64,17 @@ void goto_symext::symex_decl(statet &state, const symbol_exprt &expr)
   }
 
   // L2 renaming
-  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);
+  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;