From 55d45a0bc06ac09cdc0dbf8a63dfbecf5aec63a3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 27 Feb 2018 19:17:28 +0000
Subject: [PATCH 1/3] Test actually works fine, no bug known here

---
 regression/goto-instrument/slice19/test.desc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc
index 03cff4a4fac..3793f7374e1 100644
--- a/regression/goto-instrument/slice19/test.desc
+++ b/regression/goto-instrument/slice19/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$

From 1b65ef984d3196bb33a1ddec98fb132b1cdbc812 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 29 Nov 2016 14:42:18 +0000
Subject: [PATCH 2/3] Revert "Fixed some array and pointer reads\writes not
 appearing"

This reverts commit 55d129761bd06033af036e1585cdf411782509d2.

Pointers require dereferencing, and taking an address of an object does
not induce any reads on the object.
---
 src/analyses/goto_rw.cpp | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index be0f162c539..57174dc8e24 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -127,8 +127,6 @@ void rw_range_sett::get_objects_dereference(
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);
-  if(mode!=get_modet::READ)
-    get_objects_rec(mode, pointer);
 }
 
 void rw_range_sett::get_objects_byte_extract(
@@ -413,14 +411,13 @@ void rw_range_sett::get_objects_typecast(
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id()==ID_string_constant ||
+  if(object.id()==ID_symbol ||
+     object.id()==ID_string_constant ||
      object.id()==ID_label ||
      object.id()==ID_array ||
      object.id()=="NULL-object")
     // constant, nothing to do
     return;
-  else if(object.id()==ID_symbol)
-    get_objects_rec(get_modet::READ, object);
   else if(object.id()==ID_dereference)
     get_objects_rec(get_modet::READ, object);
   else if(object.id()==ID_index)
@@ -563,11 +560,6 @@ void rw_range_sett::get_objects_rec(
   {
     // dereferencing may yield some weird ones, ignore these
   }
-  else if(mode==get_modet::LHS_W)
-  {
-    forall_operands(it, expr)
-      get_objects_rec(mode, *it);
-  }
   else
     throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
 }

From 33c9f8909864294aad77f196c2b9818ff61ce2ad Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 27 Feb 2018 18:25:35 +0000
Subject: [PATCH 3/3] 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.
---
 regression/goto-instrument/slice24/main.c    | 14 ++++++++++++++
 regression/goto-instrument/slice24/test.desc |  6 ++++++
 src/analyses/goto_rw.cpp                     | 12 ++++++++++++
 3 files changed, 32 insertions(+)
 create mode 100644 regression/goto-instrument/slice24/main.c
 create mode 100644 regression/goto-instrument/slice24/test.desc

diff --git a/regression/goto-instrument/slice24/main.c b/regression/goto-instrument/slice24/main.c
new file mode 100644
index 00000000000..6b8156f3aa6
--- /dev/null
+++ b/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;
+}
diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice24/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 57174dc8e24..3b6fdd5c493 100644
--- a/src/analyses/goto_rw.cpp
+++ b/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(