goto-symex: initialisation of pointers is no longer necessary

goto-symex now treats empty value sets as dereferences to all current
objects. Therefore, there is no need to initialise the value set for
pointer-typed objects upon declaration.

Author: tautschnig

regression/cbmc/nondet-pointer/nondet-pointer1.c

@@ -5,9 +5,13 @@ int main()
   int x = 123;
   int *p = &x;
   int *q = nondet_pointer();
+  int *r;
 
   if(p == q)
     __CPROVER_assert(*q == 123, "value of *q");
 
+  if(p == r)
+    __CPROVER_assert(*r == 123, "value of *q");
+
   return 0;
 }

src/goto-symex/goto_symex_state.cpp

@@ -820,21 +820,6 @@ ssa_exprt goto_symex_statet::declare(ssa_exprt ssa, const namespacet &ns)
   rename(ssa.type(), l1_identifier, ns);
   ssa.update_type();
 
-  // in case of pointers, put something into the value set
-  if(ssa.type().id() == ID_pointer)
-  {
-    exprt rhs;
-    if(
-      auto failed =
-        get_failed_symbol(to_symbol_expr(ssa.get_original_expr()), ns))
-      rhs = address_of_exprt(*failed, to_pointer_type(ssa.type()));
-    else
-      rhs = exprt(ID_invalid);
-
-    exprt l1_rhs = rename<L1>(std::move(rhs), ns).get();
-    value_set.assign(ssa, l1_rhs, ns, true, false);
-  }
-
   // L2 renaming
   const exprt fields = field_sensitivity.get_fields(ns, *this, ssa);
   for(const auto &l1_symbol : find_symbols(fields))