Merge pull request #795 from tautschnig/array-replace

Implement C library string functions via array_{copy,replace,set}

Author: kroening

regression/cbmc/byte_update8/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x=0x01020304;
+  short *p=((short*)&x)+1;
+  *p=0xABCD;
+  assert(x==0xABCD0304);
+  p=(short*)(((char*)&x)+1);
+  *p=0xABCD;
+  assert(x==0xABABCD04);
+}

regression/cbmc/byte_update8/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/byte_update9/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x=0x01020304;
+  short *p=((short*)&x)+1;
+  *p=0xABCD;
+  assert(x==0x0102ABCD);
+  p=(short*)(((char*)&x)+1);
+  *p=0xABCD;
+  assert(x==0x01ABCDCD);
+}

regression/cbmc/byte_update9/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--big-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/little-endian-array1/main.c

@@ -0,0 +1,30 @@
+#include <stdlib.h>
+
+int *array;
+
+int main()
+{
+  unsigned size;
+  __CPROVER_assume(size==1);
+
+  // produce unbounded array that does not have byte granularity
+  array=malloc(size*sizeof(int));
+  array[0]=0x01020304;
+
+  int array0=array[0];
+  __CPROVER_assert(array0==0x01020304, "array[0] matches");
+
+  char *p=(char *)array;
+  char p0=p[0];
+  char p1=p[1];
+  char p2=p[2];
+  char p3=p[3];
+  __CPROVER_assert(p0==4, "p[0] matches");
+  __CPROVER_assert(p1==3, "p[1] matches");
+  __CPROVER_assert(p2==2, "p[2] matches");
+  __CPROVER_assert(p3==1, "p[3] matches");
+
+  unsigned short *q=(unsigned short *)array;
+  unsigned short q0=q[0];
+  __CPROVER_assert(q0==0x0304, "p[0,1] matches");
+}

regression/cbmc/little-endian-array1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--little-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/memset1/main.c

@@ -0,0 +1,29 @@
+#include <string.h>
+#include <stdlib.h>
+#include <assert.h>
+
+int main()
+{
+  int A[5];
+  memset(A, 0, sizeof(int)*5);
+  assert(A[0]==0);
+  assert(A[1]==0);
+  assert(A[2]==0);
+  assert(A[3]==0);
+  assert(A[4]==0);
+
+  A[3]=42;
+  memset(A, 0xFFFFFF01, sizeof(int)*3);
+  assert(A[0]==0x01010101);
+  assert(A[1]==0x01010111);
+  assert(A[2]==0x01010101);
+  assert(A[3]==42);
+  assert(A[4]==0);
+
+  int *B=malloc(sizeof(int)*2);
+  memset(B, 2, sizeof(int)*2);
+  assert(B[0]==0x02020202);
+  assert(B[1]==0x02020202);
+
+  return 0;
+}

regression/cbmc/memset1/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[main.assertion.7\] assertion A\[1\]==0x01010111: FAILURE
+\*\* 1 of 12 failed \(2 iterations\)
+--
+^warning: ignoring

src/ansi-c/ansi_c_internal_additions.cpp

@@ -244,7 +244,11 @@ void ansi_c_internal_additions(std::string &code)
     // arrays
     // NOLINTNEXTLINE(whitespace/line_length)
     "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n"
+    // overwrite all of *dest (possibly using nondet values), even
+    // if *src is smaller
     "void __CPROVER_array_copy(const void *dest, const void *src);\n"
+    // replace at most size-of-*src bytes in *dest
+    "void __CPROVER_array_replace(const void *dest, const void *src);\n"
     "void __CPROVER_array_set(const void *dest, ...);\n"
 
     // k-induction

src/ansi-c/c_typecheck_expr.cpp

@@ -2473,10 +2473,12 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt pointer_offset_expr=exprt(ID_pointer_offset, expr.type());
-    pointer_offset_expr.operands()=expr.arguments();
+    exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
     pointer_offset_expr.add_source_location()=source_location;
 
+    if(expr.type()!=pointer_offset_expr.type())
+      pointer_offset_expr.make_typecast(expr.type());
+
     return pointer_offset_expr;
   }
   else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")