Do not assign to objects that have gone out of scope

Pointer dereferencing may yield objects that have meanwhile gone out of scope.
Assigning to them is unnecessary, and performing a merge on those would yield
inconsistent equations (as witnessed by the included regression test).

Filtering out the merge in phi nodes is not easily possible as there are several
cases where it is permissible that only one of the states entering the phi node
has an (L1) object, such as declarations only seen in one branch.

Fixes: #1115

Author: tautschnig

regression/cbmc/Local_out_of_scope3/main.c

@@ -0,0 +1,24 @@
+unsigned int *GLOBAL_POINTER[1];
+
+int index;
+
+void f(void)
+{
+  unsigned int actual=0u;
+  GLOBAL_POINTER[0] = &actual;
+
+  if(index==0)
+    *GLOBAL_POINTER[index] = 1u;
+  else
+    actual = 2u;
+
+  __CPROVER_assume(1u == actual);
+}
+
+void main(void)
+{
+  index=nondet_int();
+  f();
+  f();
+  __CPROVER_assert(0==1, "");
+}

regression/cbmc/Local_out_of_scope3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-symex/symex_assign.cpp

@@ -209,6 +209,17 @@ void goto_symext::symex_assign_symbol(
   guardt &guard,
   assignment_typet assignment_type)
 {
+  // do not assign to L1 objects that have gone out of scope --
+  // pointer dereferencing may yield such objects; parameters do not
+  // have an L2 entry set up beforehand either, so exempt them from
+  // this check (all other L1 objects should have seen a declaration)
+  const symbolt *s;
+  if(!ns.lookup(lhs.get_object_name(), s) &&
+     !s->is_parameter &&
+     !lhs.get_level_1().empty() &&
+     state.level2.current_count(lhs.get_identifier())==0)
+    return;
+
   exprt ssa_rhs=rhs;
 
   // put assignment guard into the rhs