From 577706252fe342b14e3f0d16ba6f89cb69c92041 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Tue, 12 Sep 2017 20:53:23 +0100
Subject: [PATCH] check that memory for memcpy, memset and memmove is
 accessible

---
 regression/cbmc/memset3/main.c    | 12 ++++++++++++
 regression/cbmc/memset3/test.desc | 10 ++++++++++
 src/ansi-c/library/string.c       |  8 ++++++++
 3 files changed, 30 insertions(+)
 create mode 100644 regression/cbmc/memset3/main.c
 create mode 100644 regression/cbmc/memset3/test.desc

diff --git a/regression/cbmc/memset3/main.c b/regression/cbmc/memset3/main.c
new file mode 100644
index 00000000000..baedd956f62
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc
new file mode 100644
index 00000000000..0c1bb9e7ab4
--- /dev/null
+++ b/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
diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
index 9145059ff0f..87eecf42c31 100644
--- a/src/ansi-c/library/string.c
+++ b/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);