Fix goto-symex' auto-objects feature

The included test also demonstrates how to use it.

Author: tautschnig

regression/cbmc/auto_objects1/main.c

@@ -0,0 +1,13 @@
+int main()
+{
+  int *auto_object_source1;
+#pragma CPROVER check push
+#pragma CPROVER check disable "pointer"
+  if(auto_object_source1 != 0)
+    int dummy = *auto_object_source1; // triggers creating an auto object
+#pragma CPROVER check pop
+  if(auto_object_source1 != 0 && *auto_object_source1 == 42) // uses auto object
+  {
+    __CPROVER_assert(*auto_object_source1 == 42, "42");
+  }
+}

regression/cbmc/auto_objects1/test.desc

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

src/goto-symex/auto_objects.cpp

@@ -85,11 +85,14 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       {
         const symbolt &symbol = ns.lookup(obj_identifier);
 
-        if(symbol.base_name.starts_with("symex::auto_object"))
+        if(
+          symbol.base_name.starts_with("symex::auto_object") ||
+          symbol.base_name.starts_with("auto_object"))
         {
           // done already?
-          if(!state.get_level2().current_names.has_key(
-               ssa_expr.get_identifier()))
+          auto l2_index =
+            state.get_level2().current_names.find(ssa_expr.get_identifier());
+          if(!l2_index.has_value() || l2_index->get().second == 1)
           {
             initialize_auto_object(e, state);
           }

src/goto-symex/symex_dereference.cpp

@@ -321,6 +321,9 @@ void goto_symext::dereference_rec(
 
     tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), false);
 
+    // this may yield a new auto-object
+    trigger_auto_object(tmp1, state);
+
     // we need to set up some elaborate call-backs
     symex_dereference_statet symex_dereference_state(state, ns);
 
@@ -337,10 +340,6 @@ void goto_symext::dereference_rec(
       dereference.dereference(tmp1, symex_config.show_points_to_sets);
     // std::cout << "**** " << format(tmp2) << '\n';
 
-
-    // this may yield a new auto-object
-    trigger_auto_object(tmp2, state);
-
     // Check various conditions for when we should try to cache the expression.
     // 1. Caching dereferences must be enabled.
     // 2. Do not cache inside LHS of writes.