From 27227ccd96e9318c0b35f5c3049a7f75f6db2096 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 24 Mar 2017 12:58:06 +0000
Subject: [PATCH 1/2] added support for array_copy in the full-slice option

Do not slice away array_copy expressions during the implicit call
in the full-slicert class. We do not process array_copy in value_set_fit.
---
 src/goto-instrument/full_slicer.cpp   | 4 ++++
 src/pointer-analysis/value_set_fi.cpp | 3 +++
 2 files changed, 7 insertions(+)

diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 59bda7f0af0..f7b42a0af3c 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -337,6 +337,10 @@ static bool implicit(goto_programt::const_targett target)
 {
   // some variables are used during symbolic execution only
 
+  const irep_idt &statement=target->code.get_statement();
+  if(statement==ID_array_copy)
+    return true;
+
   if(!target->is_assign())
     return false;
 
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 125a2cae58a..55542296c48 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1729,6 +1729,9 @@ void value_set_fit::apply_code(
   else if(statement==ID_fence)
   {
   }
+  else if(statement==ID_array_copy)
+  {
+  }
   else if(statement==ID_input || statement==ID_output)
   {
     // doesn't do anything

From e70aa7d261f3b721d1844c5f4f498bb82b59ebc3 Mon Sep 17 00:00:00 2001
From: Lucas Cordeiro <lucasccordeiro@gmail.com>
Date: Fri, 24 Mar 2017 12:55:12 +0000
Subject: [PATCH 2/2] added two test cases into goto-instrument regression for
 checking array_copy

added two test cases related to array copy in the goto-instrument
regression suite to further test the full-slice option
---
 regression/goto-instrument/slice22/main.c    | 19 +++++++++++++++
 regression/goto-instrument/slice22/test.desc |  6 +++++
 regression/goto-instrument/slice23/main.c    | 25 ++++++++++++++++++++
 regression/goto-instrument/slice23/test.desc |  6 +++++
 4 files changed, 56 insertions(+)
 create mode 100644 regression/goto-instrument/slice22/main.c
 create mode 100644 regression/goto-instrument/slice22/test.desc
 create mode 100644 regression/goto-instrument/slice23/main.c
 create mode 100644 regression/goto-instrument/slice23/test.desc

diff --git a/regression/goto-instrument/slice22/main.c b/regression/goto-instrument/slice22/main.c
new file mode 100644
index 00000000000..bac167b63d3
--- /dev/null
+++ b/regression/goto-instrument/slice22/main.c
@@ -0,0 +1,19 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *ptr=malloc(sizeof(int));
+  *ptr=42;
+  ptr=realloc(ptr, 20);
+  assert(*ptr==42);
+
+  int *ptr2=malloc(2*sizeof(int));
+  *ptr2=42;
+  *(ptr2+1)=42;
+  ptr2=realloc(ptr2, 20);
+  assert(*ptr2==42);
+  assert(*(ptr2+1)==42);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice22/test.desc b/regression/goto-instrument/slice22/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice22/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
diff --git a/regression/goto-instrument/slice23/main.c b/regression/goto-instrument/slice23/main.c
new file mode 100644
index 00000000000..d165e2c38b8
--- /dev/null
+++ b/regression/goto-instrument/slice23/main.c
@@ -0,0 +1,25 @@
+#include <stdlib.h>
+#include <assert.h>
+
+void foo(int argc)
+{
+  void* x=0;
+
+  if(argc>3)
+    x=malloc(4*sizeof(int));
+  else
+    x=malloc(3*sizeof(int));
+  *(int*)x=42;
+
+  x=realloc(x, sizeof(int));
+
+  assert(*(int*)x==42);
+}
+
+int main(int argc, char* argv[])
+{
+//__CPROVER_ASYNC_1:
+  foo(argc);
+
+  return 0;
+}
diff --git a/regression/goto-instrument/slice23/test.desc b/regression/goto-instrument/slice23/test.desc
new file mode 100644
index 00000000000..50181efa86b
--- /dev/null
+++ b/regression/goto-instrument/slice23/test.desc
@@ -0,0 +1,6 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$