Merge pull request #2276 from tautschnig/c-string-zero

Zero-length C string operations should not yield pointer checks

Author: tautschnig

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];