moved regressions from CVS

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

regression/cbmc/ASHR1/main.c

@@ -0,0 +1,21 @@
+int main()
+{
+  int x=-4, y;
+  // should succeed
+  y=x>>1;
+  x>>=1;
+  assert(x==-2);
+  assert(y==-2);
+  
+  // should also work with mixed types
+  assert(((-2)>>1u)==-1);
+
+  // more arithmetic shifts for negative numbers  
+  x=-1;
+  x=x>>1;  
+  assert(x==-1);
+  
+  x=-10;
+  x=x>>10;
+  assert(x==-1);  
+}

regression/cbmc/ASHR1/test.desc

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

regression/cbmc/Bool1/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+
+int main() {
+  _Bool b1, b2, b3;
+  
+  b1=0;
+  b1++;
+  assert(b1);
+  
+  b2=1;
+  b2+=10;
+  assert(b2);
+  
+  b3=b1+b2;
+  assert(b3==1);
+  
+  // a struct of _Bool
+  struct
+  {
+    _Bool f1, f2, f3;
+    _Bool f4: 1, f5: 1;
+  } s;
+
+  assert(sizeof(s)==4);
+  
+  s.f1=2;
+  assert(s.f1==1);
+  
+  s.f4=1;
+  assert(s.f4);
+  
+  *((unsigned char *)(&s.f2))=1;
+  assert(s.f2);
+}

regression/cbmc/Bool1/test.desc

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

regression/cbmc/Error_Label1/main.c

@@ -0,0 +1,11 @@
+int main()
+{
+  int i;
+
+  // this should fail  
+  goto ERROR;
+
+  return 0;
+
+  ERROR:;
+}

regression/cbmc/Error_Label1/test.desc

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

regression/cbmc/Global_Initialization1/main.c

@@ -0,0 +1,24 @@
+int x = 123;
+int y;
+
+// should also work through a typedef
+typedef unsigned char uchar;
+uchar b[] = "abc";
+
+// addresses are constants
+int *p=&y;
+
+int some_func()
+{
+  static int some_static; // zero initialized
+  return some_static;
+}
+
+int main()
+{
+  assert(x == 123);
+  assert(y == 0);
+  assert(b[0]=='a');
+  assert(some_func()==0);  
+  assert(p==&y);
+}

regression/cbmc/Global_Initialization1/test.desc

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

regression/cbmc/Negation1/main.c

@@ -0,0 +1,18 @@
+int test;
+
+int main()
+{
+  test=0;
+  test=~test;
+  assert(test==-1);
+  
+  test=0;
+  test=!test;
+  assert(test==1);
+  
+  test=100;
+  test=!test;
+  assert(test==0);
+
+  assert(!!100==1);
+}

regression/cbmc/Negation1/test.desc

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

regression/cbmc/Overflow_Addition1/main.c

@@ -0,0 +1,7 @@
+int main() {
+  signed int i, j;
+  
+  i=j;
+  
+  i++;
+}

regression/cbmc/Overflow_Addition1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--signed-overflow-check
+^SIGNAL=0$
+^Counterexample:$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/Overflow_Multiplication1/falsealarm.c

@@ -0,0 +1,13 @@
+// From Cousot's FMSD paper
+
+void main()
+{
+  int x, y, _x, _y;
+
+  x=_x;
+  y=_y;
+  
+  if((-4681 < y) && (y < 4681) && (x < 32767) &&
+     (-32767 < x) && ((7*y*y -1) == x*x))
+  { y=1/x; }
+}

regression/cbmc/Overflow_Multiplication1/test.desc

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

regression/cbmc/Typecast1/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  assert(((long long int)(unsigned long long)-1)==-1);
+
+  int a;
+  __CPROVER_assume(a==-1);
+  unsigned long long x = (unsigned long long) a;
+  assert(x == -1);
+  return 0;
+}

regression/cbmc/Typecast1/test.desc

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

regression/cbmc/abs1/main.c

@@ -0,0 +1,22 @@
+double fabs(double);
+int abs(int);
+int isnan(double);
+
+int main()
+{
+  int my_i, iabs;
+  double my_d, dabs;
+  
+  assert(abs(-1)==1);
+  assert(abs(1)==1);
+  assert(fabs(1.0)==1);
+  assert(fabs(-1.0)==1);
+  
+  iabs=(my_i<0)?-my_i:my_i;
+  assert(abs(my_i)==iabs);
+
+  __CPROVER_assume(!isnan(my_d));
+ 
+  dabs=(my_d<0)?-my_d:my_d;
+  assert(fabs(my_d)==dabs);
+}

regression/cbmc/abs1/test.desc

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

regression/cbmc/argv1/main.c

@@ -0,0 +1,11 @@
+int main(int argc, char **argv)
+{
+  char *x;
+
+  // there must be at least one
+  x=argv[0];
+  assert(argc>=1);
+
+  // last one must be NULL
+  assert(argv[argc]==0);
+}

regression/cbmc/argv1/test.desc

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

regression/cbmc/exit1/main.c

@@ -0,0 +1,11 @@
+void exit(int status);
+
+int main() {
+  int x;
+  
+  if(x==10)
+    exit(1);
+
+  if(x==10)
+    assert(0);
+}

regression/cbmc/exit1/test.desc

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

regression/cbmc/for-break1/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int a=0, b=0;
+  int x;
+
+  for(x=0; x<3; x++)
+  {
+    break;
+
+    b=1;
+  }
+ 
+  assert(a==b);
+}

regression/cbmc/for-break1/test.desc

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

regression/cbmc/gcc_conditional_expr1/main.c

@@ -0,0 +1,17 @@
+int g, k;
+
+int main()
+{
+  int r1, r2;
+  
+  r1= (g++) ? : 2;
+  
+  assert(r1==2);
+  assert(g==1);
+
+  r2= (g++) ? : (k++);
+  
+  assert(r2==1);
+  assert(g==2);  
+  assert(k==0);
+}

regression/cbmc/gcc_conditional_expr1/test.desc

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

regression/cbmc/gcc_local_label1/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+// GCC has 'local labels', visible only in their respective block
+void other_f()
+{
+  int x;
+
+  #ifdef __GNUC__
+  here:;
+  x++;
+  
+  {
+    __label__ here, there;
+    
+    goto here; // not jumping up, but down!
+
+    here:; // this would usually fail
+    
+    assert(0);
+  }
+  #else
+  // I don't know a Visual Studio equivalent
+  assert(0);
+  #endif
+}
+
+int main()
+{
+  other_f();
+}
+

regression/cbmc/gcc_local_label1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 1 --no-unwinding-assertions
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/goto1/main.c

@@ -0,0 +1,14 @@
+int main()
+{
+  int i, j;
+  
+  if(i)
+    goto l;
+    
+  if(j)
+    goto l;
+    
+  assert(!i && !j);
+ 
+ l:; 
+}

regression/cbmc/goto1/test.desc

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

regression/cbmc/goto2/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int i, j;
+
+  i=1;
+
+  if(j)
+    goto l;
+
+  i=2;
+ 
+ l:; 
+ 
+  assert(i==1 || !j);
+}

regression/cbmc/goto2/test.desc

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

regression/cbmc/goto3/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int i;
+  
+  i=0;
+
+loop:
+  assert(i<10);
+  i++;
+  
+  if(i<10)
+    goto loop;
+  
+  assert(i==10);
+}

regression/cbmc/goto3/test.desc

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

regression/cbmc/goto4/main.c

@@ -0,0 +1,15 @@
+int g=0;
+
+int f()
+{
+  assert(g==0);
+  g++;
+}
+
+int main()
+{
+l:
+l2:;
+  int i=f();
+  goto l;
+}

regression/cbmc/goto4/test.desc

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

regression/cbmc/inline1/header.h

@@ -0,0 +1,9 @@
+int x;
+
+// this is C99 compliant,
+// see http://stackoverflow.com/questions/216510/extern-inline
+static inline void f()
+{
+  x=1;
+}
+

regression/cbmc/inline1/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+
+#include "header.h"
+
+int main()
+{
+  f();
+  assert(x==1);
+}

regression/cbmc/inline1/module.c

@@ -0,0 +1 @@
+#include "header.h"

regression/cbmc/inline1/test.desc

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

regression/cbmc/return1/main.c

@@ -0,0 +1,45 @@
+
+short  ret_const()
+{
+  return 123;
+}
+
+
+unsigned long save_res0, save_res1;
+
+
+int f0()
+{
+  short res = 0;
+
+  res += ret_const();  // <-- fails
+  //res = ret_const();   // <-- OK
+  //res += 123;          // <-- OK
+
+  save_res0 = res;
+
+  return 0;
+}
+
+
+int f1()
+{
+  short res = 0;
+
+  res += ret_const();  // <-- fails
+  //res = ret_const();   // <-- OK
+  //res += 123;          // <-- OK
+
+  save_res1 = res;
+
+  return 0;
+}
+
+
+int main()
+{
+  f0();
+  f1();
+
+  assert( save_res0 == save_res1 );
+}

regression/cbmc/return1/test.desc

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

regression/cbmc/return3/main.c

@@ -0,0 +1,21 @@
+unsigned nondet_uint();
+
+int new_intu(unsigned int lower, unsigned int upper)
+{
+  unsigned int val = (unsigned) 1u << 31;
+
+  if (val < lower)
+    return lower;
+
+  if (val > upper)
+    return upper;
+
+  return val;
+}
+
+
+int main()
+{
+  unsigned int i1 = new_intu(1u, 31u);
+  assert(1 <= i1 && i1 <= 31);
+}

regression/cbmc/return3/test.desc

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

regression/cbmc/return4/main.c

@@ -0,0 +1,106 @@
+short f0(short x)
+{
+  int z;
+
+  do {
+    z=0;
+    if(x <= 0) { z=1;
+      return 100; }
+  }
+  while( x-- ); /* <-- The diff */
+
+  z=2;
+  return 200;
+}
+
+short f1(short x)
+{
+  do {
+    if(x <= 0)
+      return 100;
+  }
+  while( --x ); /* <-- The diff */
+
+  return 200;
+}
+
+
+short f0_if(short x)
+{
+  if( x-- )
+    return 200;
+
+  if(x <= 0)
+    return 100;
+
+  return 0;
+}
+
+short f1_if(short x)
+{
+  if( --x )
+    return 200;
+
+  if(x <= 0)
+    return 100;
+
+  return 0;
+}
+
+
+short f0_wh(short x)
+{
+  while( x-- )  /* <-- The diff */
+    if(x <= 0)
+      return 100;
+
+  return 200;
+}
+
+short f1_wh(short x)
+{
+  while( --x )  /* <-- The diff */
+    if(x <= 0)
+      return 100;
+
+  return 200;
+}
+
+
+int main()
+{
+  int flag;
+  short a;
+  short res0, res1;
+
+  if( flag )
+    a = 1;
+  else
+    a = 1;
+
+  res0 = f0(a);
+  res1 = f1(a);
+
+  assert(res0==100);
+  assert(res1==200);
+
+  res0 = f0(a);
+  res1 = f1(a);
+
+  assert(res0==100);
+  assert(res1==200);
+
+  res0 = f0_if(a);
+  res1 = f1_if(a);
+
+  assert(res0==200);
+  assert(res1==100);
+
+  res0 = f0_wh(a);
+  res1 = f1_wh(a);
+
+  assert(res0==100);
+  assert(res1==200);
+
+  return 0;
+}

regression/cbmc/return4/test.desc

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

regression/cbmc/return5/main.c

@@ -0,0 +1,44 @@
+short f0(short x)
+{
+  int z;
+
+  do {
+    z=0;
+    if(x <= 0) { z=1;
+      return 100; }
+  }
+  while( x-- ); /* <-- The diff */
+
+  z=2;
+  return 200;
+}
+
+short f1(short x)
+{
+  do {
+    if(x <= 0)
+      return 100;
+  }
+  while( --x ); /* <-- The diff */
+
+  return 200;
+}
+
+int main()
+{
+  int flag;
+  short a;
+  short res0, res1;
+
+  if( flag )
+    a = 1;
+  else
+    a = 1;
+
+  res0 = f0(a);
+  res1 = f1(a);
+
+  assert(res0 == res1); /* <-- should fail */
+  
+  return 0;
+}

regression/cbmc/return5/test.desc

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

regression/cbmc/void_ifthenelse/main.c

@@ -0,0 +1,14 @@
+int g;
+
+void f()
+{
+  g=1;
+}
+
+int main() {
+  assert(g==0);
+  
+  g==0?f():g;
+
+  assert(g==1);
+}

regression/cbmc/void_ifthenelse/test.desc

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