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

Author: lucasccordeiro

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$