Do not assign to objects that have gone out of scope

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