New CBMC regression tests for unsupported features

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3536 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

regression/cbmc/Eval_Order1/main.c

@@ -0,0 +1,7 @@
+int main() {
+  int x = 0;
+  x = ++x + x;
+  // depending on the order of evaluation, the following may fail
+  assert(x == 1);
+  return 0;
+}

regression/cbmc/Eval_Order1/test.desc

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

regression/cbmc/Eval_Order2/main.c

@@ -0,0 +1,7 @@
+int main() {
+  int x = 0;
+  x = ++x + x;
+  // depending on the order of evaluation, the following may fail
+  assert(x == 2);
+  return 0;
+}

regression/cbmc/Eval_Order2/test.desc

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

regression/cbmc/Malloc12/main.c

@@ -0,0 +1,10 @@
+void * malloc(unsigned);
+
+// if the implementation of malloc is sound, this one should fail
+
+int main() {
+  char * a;
+  a = malloc(5);
+  assert(a != 0);
+  return 0;
+}

regression/cbmc/Malloc12/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+--pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/Malloc13/main.c

@@ -0,0 +1,11 @@
+void * malloc(unsigned);
+
+int main(int argc, char* argv[]) {
+  unsigned short len;
+  char * str;
+  __CPROVER_assume(len > 0);
+  str = malloc(len);
+  assert(__CPROVER_buffer_size(str) == len);
+  return 0;
+}
+

regression/cbmc/Malloc13/test.desc

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

regression/cbmc/Malloc14/main.c

@@ -0,0 +1,12 @@
+void *malloc(int);
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  if(p != (int*)0)
+  {
+    int *q = malloc(sizeof(int));
+    __CPROVER_assert (p != q, "same memory allocated twice");
+  }
+  return 0;
+}

regression/cbmc/Malloc14/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/Malloc15/main.c

@@ -0,0 +1,15 @@
+void *malloc(int);
+
+int main()
+{
+  int *p;
+
+  p = malloc(sizeof(int));
+  unsigned int r = p;
+  if (r != 0)
+    *p = 1;    
+
+  if (p != 0)
+    __CPROVER_assert (*p == 1, "malloc");
+  return 0;
+}

regression/cbmc/Malloc15/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--32
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/Malloc16/main.c

@@ -0,0 +1,25 @@
+void *malloc(int);
+
+int foo(int *x)
+{
+  *x = 1;
+}
+
+int main()
+{
+  void *tmp;
+  int *dev;
+
+  tmp = malloc(sizeof(int));
+  dev = (int*)tmp;
+  
+  void *r = (void*)0;
+  unsigned int q = r;
+  unsigned int p = dev;
+  if(p != q)
+  {
+    foo(dev);
+    __CPROVER_assert(*dev==1, "WTF?");
+  }
+  return 0;
+}

regression/cbmc/Malloc16/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--32
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/Memmove1/main.c

@@ -0,0 +1,45 @@
+#include <string.h>
+#include <assert.h>
+
+void sort_items_by_criteria( int * item, int left, int right )
+{
+  int lidx = left, ridx = (left+right)/2 + 1, lsize = (left+right)/2 - left + 1;
+  int tmp;
+
+  if ( right - left < 1 ) return;
+  sort_items_by_criteria( item, left, (left+right)/2 );
+  sort_items_by_criteria( item, (left+right)/2 + 1, right );
+
+  while ( ridx <= right && lidx < ridx ) {
+    if ( item[lidx] > item[ridx] ) {
+      tmp = item[ridx];
+      memmove( item + lidx + 1, item + lidx, lsize * sizeof(int) );
+      item[lidx] = tmp;
+      ++ridx;
+      ++lsize;
+    }
+    ++lidx;
+    --lsize;
+  }
+}
+
+int main(int argc, char * argv[]) {
+  int a[7];
+
+  //CBMC reports wrong results for 256, -2147221455, -2147221455, -2147221455, 16, -2147483600, 16384
+  a[0] = 256;
+  a[1] = -2147221455;
+  a[2] = -2147221455;
+  a[3] = -2147221455;
+  a[4] = 16;
+  a[5] = -2147483600;
+  a[6] = 16384;
+
+  sort_items_by_criteria(a, 0, 6);
+
+  printf("%d %d %d %d %d %d %d\n", a[0], a[1], a[2], a[3], a[4], a[5], a[6]);
+
+  assert(a[0]==-2147483600);
+  return 0;
+}
+

regression/cbmc/Memmove1/test.desc

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

regression/cbmc/Pointer_Assume1/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  int * a;
+  int b=1;
+  __CPROVER_assume(a == &b);
+  assert(*a==1);
+  return 0;
+}

regression/cbmc/Pointer_Assume1/test.desc

@@ -0,0 +1,7 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

regression/cbmc/Unwinding_Assertions_Improved1/main.c

@@ -0,0 +1,14 @@
+int main() {
+  int a;
+  __CPROVER_assume(a >= 4);
+  while (a > 0) {
+    --a;
+  }
+
+  // this one should be reported to fail, even with unwinding assertions turned
+  // on (first check all other claims, then unwinding assertions)
+  assert(a > 0);
+  // once the above is disabled, it should be possible to "prove" this one in
+  // that the unwinding assertion fails first
+  assert(a <= 0);
+}

regression/cbmc/Unwinding_Assertions_Improved1/test.desc

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

regression/cbmc/Variadic1/main.c

@@ -0,0 +1,41 @@
+#include <stdarg.h>
+#include <stdio.h>
+
+// how to do it:
+// once an ellipsis is seen in the called function, declare an array of
+// appropriate size (sum of sizeofs+paddings) and pass the array to the called
+// function
+// function with ellipsis has ellipsis replaced by void* pointer
+// use of va_list is turned into assignment of this pointer
+// va_start is no-op, just like va_end
+// va_arg returns casted memory at pointer and increments pointer afterwards by
+// given size (+padding)
+
+  int
+add_em_up (int count,...)
+{
+  va_list ap;
+  int i, sum;
+
+  va_start (ap, count);         /* Initialize the argument list. */
+
+  sum = 0;
+  for (i = 0; i < count; i++)
+    sum += va_arg (ap, int);    /* Get the next argument value. */
+
+  va_end (ap);                  /* Clean up. */
+  return sum;
+}
+
+  int
+main (void)
+{
+  /* This call prints 16. */
+  assert(16 == add_em_up (3, 5, 5, 6));
+
+  /* This call prints 55. */
+  assert(55 == add_em_up (10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10));
+
+  return 0;
+}
+

regression/cbmc/Variadic1/test.desc

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

regression/cbmc/Volatile1/main.c

@@ -0,0 +1,6 @@
+volatile int x;
+int main() {
+  if (!x)
+    assert(!x);
+}
+

regression/cbmc/Volatile1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cpp/sizeof3/main.cpp

@@ -0,0 +1,10 @@
+int iDebugRec [20] ;
+
+void bar() {
+  unsigned s;
+  s=sizeof(iDebugRec);
+  s=sizeof(iDebugRec[0]);
+  iDebugRec[0]=1;
+}
+
+

regression/cpp/sizeof3/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--