goto_rw: treat dereference failure as a read/write of __CPROVER_memory

Treating any such access as an access to the single, global memory object will
enable sound overapproximation, and thus helps slicing soundness.

Author: tautschnig

regression/goto-instrument/slice24/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static void f(int* x) { *x = 5; }
+static void g(int *x) { assert(*x == 5); }
+
+int main(int argc, char** argv) {
+
+  int *x = (int*)malloc(sizeof(int));
+  f(x);
+  g(x);
+
+  return 0;
+}

regression/goto-instrument/slice24/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$

src/analyses/goto_rw.cpp

@@ -127,6 +127,11 @@ void rw_range_sett::get_objects_dereference(
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);
+
+  // we don't have points-to information, dereferencing will yield some
+  // in-memory object
+  const symbolt &memory_symbol = ns.lookup(CPROVER_PREFIX "memory");
+  get_objects_rec(mode, memory_symbol.symbol_expr(), -1, size);
 }
 
 void rw_range_sett::get_objects_byte_extract(
@@ -612,6 +617,13 @@ void rw_range_set_value_sett::get_objects_dereference(
   if(object.is_not_nil() &&
      !value_set_dereferencet::has_dereference(object))
     get_objects_rec(mode, object, range_start, new_size);
+  else
+  {
+    // we don't have sufficient points-to information, dereferencing will yield
+    // some in-memory object
+    const symbolt &memory_symbol = ns.lookup(CPROVER_PREFIX "memory");
+    get_objects_rec(mode, memory_symbol.symbol_expr(), -1, size);
+  }
 }
 
 void guarded_range_domaint::output(