check that memory for memcpy, memset and memmove is accessible

Author: kroening

regression/cbmc/memset3/main.c

@@ -0,0 +1,12 @@
+#include <string.h>
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int *A=malloc(sizeof(int)*4);
+
+  memset(A+20, 0, sizeof(int)); // out-of-bounds
+
+  return 0;
+}

regression/cbmc/memset3/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[.*] dereference failure: pointer outside dynamic object bounds in .*: FAILURE
+\*\* 1 of .* failed \(.*\)
+--
+^warning: ignoring

src/ansi-c/library/string.c

@@ -531,6 +531,8 @@ void *memcpy(void *dst, const void *src, size_t n)
   #else
   __CPROVER_assert(__CPROVER_POINTER_OBJECT(dst)!=
                    __CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap");
+  (void)*(char *)dst; // check that the memory is accessible
+  (void)*(const char *)src; // check that the memory is accessible
   //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
   char src_n[n];
   __CPROVER_array_copy(src_n, (char*)src);
@@ -561,6 +563,8 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
   #else
   __CPROVER_assert(__CPROVER_POINTER_OBJECT(dst)!=
                    __CPROVER_POINTER_OBJECT(src), "memcpy src/dst overlap");
+  (void)*(char *)dst; // check that the memory is accessible
+  (void)*(const char *)src; // check that the memory is accessible
   (void)size;
   //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
   char src_n[n];
@@ -598,6 +602,7 @@ void *memset(void *s, int c, size_t n)
   else
     __CPROVER_is_zero_string(s)=0;
   #else
+  (void)*(char *)s; // check that the memory is accessible
   //char *sp=s;
   //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
   unsigned char s_n[n];
@@ -659,6 +664,7 @@ void *__builtin___memset_chk(void *s, int c, __CPROVER_size_t n, __CPROVER_size_
   else
     __CPROVER_is_zero_string(s)=0;
   #else
+  (void)*(char *)s; // check that the memory is accessible
   (void)size;
   //char *sp=s;
   //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
@@ -693,6 +699,8 @@ void *memmove(void *dest, const void *src, size_t n)
   else
     __CPROVER_is_zero_string(dest)=0;
   #else
+  (void)*(char *)dest; // check that the memory is accessible
+  (void)*(const char *)src;  // check that the memory is accessible
   char src_n[n];
   __CPROVER_array_copy(src_n, (char*)src);
   __CPROVER_array_replace((char*)dest, src_n);