Merge pull request #3483 from diffblue/memcpy_overlap

fix memcpy overlap check

Author: tautschnig

regression/cbmc/memcpy1/main.c renamed to regression/cbmc-library/memcpy-02/memcpy1.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+memcpy1.c
 --bounds-check --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/memcpy1/test.desc renamed to regression/cbmc-library/memcpy-02/memcpy1.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+memcpy2.c
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/memcpy2/main.c renamed to regression/cbmc-library/memcpy-02/memcpy2.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+memcpy3.c
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/memcpy2/test.desc renamed to regression/cbmc-library/memcpy-02/memcpy2.desc

@@ -0,0 +1,18 @@
+#include <string.h>
+
+int main()
+{
+  char bufferA[10], bufferB[10];
+
+  // ok
+  memcpy(bufferA, bufferB, 10);
+
+  // not ok, overlap, should use memmove
+  memcpy(bufferA, bufferA + 1, 9);
+
+  // ok, no overlap
+  memcpy(bufferA, bufferA + 5, 5);
+
+  // out of bounds
+  memcpy(bufferA + 1, bufferB, 10);
+}

regression/cbmc/memcpy3/main.c renamed to regression/cbmc-library/memcpy-02/memcpy3.c

@@ -0,0 +1,13 @@
+CORE
+memcpy4.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*] line 8 memcpy src/dst overlap: SUCCESS$
+^\[.*] line 11 memcpy src/dst overlap: FAILURE$
+^\[.*] line 14 memcpy src/dst overlap: SUCCESS$
+^\[.*] line 17 memcpy src/dst overlap: SUCCESS$
+^\[.*] line 17 memcpy destination region writeable: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/memcpy3/test.desc renamed to regression/cbmc-library/memcpy-02/memcpy3.desc

@@ -139,6 +139,7 @@ rm havoc_object1/test.desc
 rm hex_trace/test.desc
 rm integer-assignments1/test.desc
 rm little-endian-array1/test.desc
+rm memcpy/memcpy4.desc
 rm memory_allocation1/test.desc
 rm memset1/test.desc
 rm mm_io1/test.desc