Merge pull request #694 from lucasccordeiro/fix-full-slice-03

consider array_copy expressions in the full-slice

Author: kroening

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;
+}

regression/goto-instrument/slice22/test.desc

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

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;
+}

regression/goto-instrument/slice23/test.desc

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

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;
 

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