moved regressions from CVS

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

regression/cbmc/Bitfields1/main.c

@@ -0,0 +1,36 @@
+typedef int INT;
+
+typedef enum _INTEL_CACHE_TYPE {
+    IntelCacheNull,
+    IntelCacheTrace=10
+} INTEL_CACHE_TYPE;
+
+struct bft {
+  unsigned int a:3;
+  unsigned int b:1;
+
+  // an anonymous bitfield
+  signed int :2;
+  
+  // with typedef
+  INT x:1;
+  
+  // made of sizeof
+  unsigned int abc: sizeof(int);
+
+  // enums are integers!
+  INTEL_CACHE_TYPE Type : 5;
+  
+  // and good as field sizes
+  INTEL_CACHE_TYPE Field2 : IntelCacheTrace;
+};
+ 
+
+int main() {
+  struct bft bf;
+   
+  assert(bf.a<=7);
+  assert(bf.b<=1);
+  
+  bf.Type=IntelCacheTrace;
+}

regression/cbmc/Bitfields1/test.desc

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

regression/cbmc/Fixedbv1/main.c

@@ -0,0 +1,16 @@
+int main() {
+  double x;
+  int y;
+  
+  x=2;  
+  x-=0.6;
+  y=x; // this yields 1.4, which is cut off
+  
+  assert(y==1);
+
+  x=2;  
+  x-=0.4;
+  y=x; // this yields 1.6, which is cut off, too!
+  
+  assert(y==1);
+}

regression/cbmc/Fixedbv1/test.desc

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

regression/cbmc/Fixedbv2/main.c

@@ -0,0 +1,10 @@
+main() {
+        float a;
+        double b;
+
+        a=1.25L;
+        assert(a==1.25);
+
+        b=1.250;
+        assert(b==1.25);
+}

regression/cbmc/Fixedbv2/test.desc

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

regression/cbmc/Fixedbv3/main.c

@@ -0,0 +1,24 @@
+int nondet_int();
+
+double d = 0.0;
+
+void f1()
+{
+  d = 1.0;
+}
+
+int main()
+{
+  int x = 2;
+
+  if(nondet_int())
+    x = 4;
+
+  (void) f1();
+
+  d += (x == 2);
+
+  d += (x > 3);
+
+  assert(d == 2.0);
+}

regression/cbmc/Fixedbv3/test.desc

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

regression/cbmc/Fixedbv4/main.c

@@ -0,0 +1,61 @@
+int main()
+{
+  double f;
+  
+  // addition
+  assert(100.0+10==110);
+  assert(0+f==f);
+  assert(f+0==f);
+  assert(100+0.5==100.5);
+  assert(0.0+0.0+f==f);
+  
+  // subtraction
+  assert(100.0-10==90);
+  assert(0-f==-f);
+  assert(f-0==f);
+  assert(100-0.5==99.5);
+  assert(0.0-0.0-f==-f);
+
+  // unary minus
+  assert(-(-100.0)==100);
+  assert(-(1-2.0)==1);
+  assert(-(-f)==f);
+
+  // multiplication
+  assert(100.0*10==1000);
+  assert(0*f==0);
+  assert(f*0==0);
+  assert(100*0.5==50);
+  assert(f*1==f);
+  assert(1*f==f);
+  assert(1.0*1.0*f==f);
+
+  // division
+  assert(100.0/1.0==100);
+  assert(100.1/1.0==100.1);
+  assert(100.0/2.0==50);
+  assert(100.0/0.5==200);
+  assert(0/1.0==0);
+  assert(f/1.0==f);
+  
+  // conversion
+  assert(((double)(float)100)==100.0);
+  assert(((unsigned int)100.0)==100.0);
+  assert(100.0);
+  assert(!0.0);
+  assert((int)0.5==0);
+  assert((int)0.49==0);
+  assert((int)-1.5==-1);
+  assert((int)-10.49==-10);
+  
+  // relations
+  assert(1.0<2.5);
+  assert(1.0<=2.5);
+  assert(1.01<=1.01);
+  assert(2.5>1.0);
+  assert(2.5>=1.0);
+  assert(1.01>=1.01);
+  assert(!(1.0>=2.5));
+  assert(!(1.0>2.5));
+  assert(1.0!=2.5);
+}

regression/cbmc/Fixedbv4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--fixedbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+\(Starting CEGAR Loop\|VCC(s), 0 remaining after simplification$\)
+--
+^warning: ignoring

regression/cbmc/Fixedbv5/main.c

@@ -0,0 +1,10 @@
+int main()
+{
+  float a, b;
+  
+  __CPROVER_assume(a==1 || a==0.5 || a==2 || a==3 || a==0.1);
+  b=a;
+  a/=2;
+  a*=2;
+  __CPROVER_assert(a==b, "float div works");
+}

regression/cbmc/Fixedbv5/test.desc

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

regression/cbmc/Fixedbv6/main.c

@@ -0,0 +1,45 @@
+int main()
+{
+  // constants
+  assert(1.0!=2.0);
+  assert(1.0==1.0);
+  assert(1.0<2.0);
+  assert(!(-1.0<-2.0));
+  assert(2.0>1.0);
+  assert(!(-2.0>-1.0));
+  assert(!(2.0<2.0));
+  assert(!(-2.0<-2.0));
+  assert(!(2.0>2.0));
+  assert(!(-2.0>-2.0));
+  assert(2.0<=2.0);
+  assert(-2.0<=-2.0);
+  assert(2.0>=2.0);
+  assert(-2.0>=-2.0);
+  assert(1.0<=2.0);
+  assert(!(-1.0<=-2.0));
+  assert(2.0>=1.0);
+  assert(!(-2.0>=-1.0));  
+  
+  // variables
+  float a, b, _a=a, _b=b;
+  __CPROVER_assume(a==1 && b==2);
+
+  assert(a!=b);
+  assert(a==a);
+  assert(a<b);
+  assert(!(-a<-b));
+  assert(b>a);
+  assert(!(-b>-a));
+  assert(!(b<b));
+  assert(!(-b<-b));
+  assert(!(b>b));
+  assert(!(-b>-b));
+  assert(b<=b);
+  assert(-b<=-b);
+  assert(b>=b);
+  assert(-b>=-b);
+  assert(a<=b);
+  assert(!(-a<=-b));
+  assert(b>=a);
+  assert(!(-b>=-a));  
+}

regression/cbmc/Fixedbv6/test.desc

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

regression/cbmc/Fixedbv7/main.c

@@ -0,0 +1,61 @@
+int main()
+{
+  double f;
+  
+  // addition
+  assert(100.0+10==110);
+  assert(0+f==f);
+  assert(f+0==f);
+  assert(100+0.5==100.5);
+  assert(0.0+0.0+f==f);
+  
+  // subtraction
+  assert(100.0-10==90);
+  assert(0-f==-f);
+  assert(f-0==f);
+  assert(100-0.5==99.5);
+  assert(0.0-0.0-f==-f);
+
+  // unary minus
+  assert(-(-100.0)==100);
+  assert(-(1-2.0)==1);
+  assert(-(-f)==f);
+
+  // multiplication
+  assert(100.0*10==1000);
+  assert(0*f==0);
+  assert(f*0==0);
+  assert(100*0.5==50);
+  assert(f*1==f);
+  assert(1*f==f);
+  assert(1.0*1.0*f==f);
+
+  // division
+  assert(100.0/1.0==100);
+  assert(100.1/1.0==100.1);
+  assert(100.0/2.0==50);
+  assert(100.0/0.5==200);
+  assert(0/1.0==0);
+  assert(f/1.0==f);
+  
+  // conversion
+  assert(((double)(float)100)==100.0);
+  assert(((unsigned int)100.0)==100.0);
+  assert(100.0);
+  assert(!0.0);
+  assert((int)0.5==0);
+  assert((int)0.49==0);
+  assert((int)-1.5==-1);
+  assert((int)-10.49==-10);
+  
+  // relations
+  assert(1.0<2.5);
+  assert(1.0<=2.5);
+  assert(1.01<=1.01);
+  assert(2.5>1.0);
+  assert(2.5>=1.0);
+  assert(1.01>=1.01);
+  assert(!(1.0>=2.5));
+  assert(!(1.0>2.5));
+  assert(1.0!=2.5);
+}

regression/cbmc/Fixedbv7/test.desc

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