From 523f8aeba1695cd80316e75eee5ec843fa7714cb Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 5 Jun 2018 08:19:06 +0100
Subject: [PATCH] Zero-length C string operations should not yield pointer
 checks

One-past-the-end pointers are permitted in C (although they cannot be
dereferenced), and thus only check for valid start-of-string when that string
(array) is of non-zero length.
---
 src/ansi-c/library/string.c | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/ansi-c/library/string.c b/src/ansi-c/library/string.c
index 8781b77c35d..d001a5f4fef 100644
--- a/src/ansi-c/library/string.c
+++ b/src/ansi-c/library/string.c
@@ -597,11 +597,11 @@ void *memcpy(void *dst, const void *src, size_t n)
   __CPROVER_precondition(__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
 
   if(n > 0)
   {
+    (void)*(char *)dst; // check that the memory is accessible
+    (void)*(const char *)src; // check that the memory is accessible
     (void)*(((char *)dst) + n - 1);       // check that the memory is accessible
     (void)*(((const char *)src) + n - 1); // check that the memory is accessible
     //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
@@ -639,12 +639,12 @@ void *__builtin___memcpy_chk(void *dst, const void *src, __CPROVER_size_t n, __C
   __CPROVER_precondition(__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;
 
   if(n > 0)
   {
+    (void)*(char *)dst; // check that the memory is accessible
+    (void)*(const char *)src; // check that the memory is accessible
     (void)*(((char *)dst) + n - 1);       // check that the memory is accessible
     (void)*(((const char *)src) + n - 1); // check that the memory is accessible
     //for(__CPROVER_size_t i=0; i<n ; i++) ((char *)dst)[i]=((const char *)src)[i];
@@ -685,10 +685,10 @@ 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
 
   if(n > 0)
   {
+    (void)*(char *)s; // check that the memory is accessible
     (void)*(((char *)s) + n - 1); // check that the memory is accessible
     //char *sp=s;
     //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
@@ -724,10 +724,10 @@ void *__builtin_memset(void *s, int c, __CPROVER_size_t n)
     __CPROVER_is_zero_string(s)=0;
   }
   #else
-  (void)*(char *)s; // check that the memory is accessible
 
   if(n > 0)
   {
+    (void)*(char *)s; // check that the memory is accessible
     (void)*(((char *)s) + n - 1); // check that the memory is accessible
     //char *sp=s;
     //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
@@ -763,11 +763,11 @@ 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;
 
   if(n > 0)
   {
+    (void)*(char *)s; // check that the memory is accessible
     (void)*(((char *)s) + n - 1); // check that the memory is accessible
     //char *sp=s;
     //for(__CPROVER_size_t i=0; i<n ; i++) sp[i]=c;
@@ -804,11 +804,11 @@ 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
 
   if(n > 0)
   {
+    (void)*(char *)dest; // check that the memory is accessible
+    (void)*(const char *)src;  // check that the memory is accessible
     (void)*(((char *)dest) + n - 1);      // check that the memory is accessible
     (void)*(((const char *)src) + n - 1); // check that the memory is accessible
     char src_n[n];
@@ -848,12 +848,12 @@ void *__builtin___memmove_chk(void *dest, const void *src, size_t n, __CPROVER_s
     __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
   (void)size;
 
   if(n > 0)
   {
+    (void)*(char *)dest; // check that the memory is accessible
+    (void)*(const char *)src;  // check that the memory is accessible
     (void)*(((char *)dest) + n - 1);      // check that the memory is accessible
     (void)*(((const char *)src) + n - 1); // check that the memory is accessible
     char src_n[n];