Move CBMC float tests to main regression folder

ultimate-pa · Jan 16, 2023 · 19af9de · 19af9de
1 parent 2da9514
commit 19af9de
Show file tree

Hide file tree

Showing 32 changed files with 329 additions and 117 deletions.
diff --git a/...at-flags-simp1_true-unreach-call__PART1.i → ...ression/c/cbmc_float-flags-simp1__PART1.i b/...at-flags-simp1_true-unreach-call__PART1.i → ...ression/c/cbmc_float-flags-simp1__PART1.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 
 

diff --git a/...at-flags-simp1_true-unreach-call__PART2.i → ...ression/c/cbmc_float-flags-simp1__PART2.i b/...at-flags-simp1_true-unreach-call__PART2.i → ...ression/c/cbmc_float-flags-simp1__PART2.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 
 

diff --git a/...at-flags-simp1_true-unreach-call__PART3.i → ...ression/c/cbmc_float-flags-simp1__PART3.i b/...at-flags-simp1_true-unreach-call__PART3.i → ...ression/c/cbmc_float-flags-simp1__PART3.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 
 

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-no-simp1_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-no-simp1_.i
@@ -0,0 +1,20 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+int main()
+{
+  unsigned int i, j;
+  double d;
+
+  i=100.0;
+  d=i;
+  j=d;
+  if(!(j==100)) __VERIFIER_error();
+}
diff --git a/..._true-unreach-call__COMMENTED_DIFFICULT.i → ...bmc_float-no-simp2__COMMENTED_DIFFICULT.i b/..._true-unreach-call__COMMENTED_DIFFICULT.i → ...bmc_float-no-simp2__COMMENTED_DIFFICULT.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_assume(int);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_assume(int);
 
 
 

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-no-simp3_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-no-simp3_.i
@@ -0,0 +1,18 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+
+int main()
+{
+
+  float fs1=2.0f/6.0f;
+  float fs2=fs1*6.0f;
+  if(!((int)fs2==2)) __VERIFIER_error();
+}
diff --git a/...ession/float-no-simp4_true-unreach-call.i → ...Point/regression/c/cbmc_float-no-simp4_.i b/...ession/float-no-simp4_true-unreach-call.i → ...Point/regression/c/cbmc_float-no-simp4_.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_assume(int);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_assume(int);
 
 
 

diff --git a/...ession/float-no-simp6_true-unreach-call.i → ...Point/regression/c/cbmc_float-no-simp6_.i b/...ession/float-no-simp6_true-unreach-call.i → ...Point/regression/c/cbmc_float-no-simp6_.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 void multiply(void)
 {

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-no-simp7_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-no-simp7_.i
@@ -0,0 +1,22 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+
+int main (int argc, char **argv) {
+  float f = 0x1.9e0c22p-101f;
+  float g = -0x1.3c9014p-50f;
+  float target = -0x1p-149f;
+
+  float result = f * g;
+
+  if(!(result == target)) __VERIFIER_error();
+
+  return 0;
+}
diff --git a/...ession/float-no-simp8_true-unreach-call.i → ...Point/regression/c/cbmc_float-no-simp8_.i b/...ession/float-no-simp8_true-unreach-call.i → ...Point/regression/c/cbmc_float-no-simp8_.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 
 

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-to-double2_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float-to-double2_.i
@@ -0,0 +1,21 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+
+int main(void)
+{
+  float f = -0x1.0p-127f;
+  double d = -0x1.0p-127;
+  double fp = (double)f;
+
+  if(!(d == fp)) __VERIFIER_error();
+
+  return 0;
+}
diff --git a/...mc-regression/float11_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float11_.i b/...mc-regression/float11_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float11_.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 int main()
 {
 

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float12_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float12_.i
@@ -0,0 +1,21 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+int main()
+{
+  float f;
+  double d;
+  unsigned char x;
+
+  d=f;
+
+  if(f==x)
+    if(!(d==x)) __VERIFIER_error();
+}
diff --git a/...mc-regression/float13_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float13_.i b/...mc-regression/float13_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float13_.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 const float plus_infinity = 1.0f/0.0f;
 const float minus_infinity = 0.0f/-0.0f;

diff --git a/...mc-regression/float14_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float14_.i b/...mc-regression/float14_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float14_.i
@@ -1,4 +1,13 @@
+//#Safe
 
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+
 
 
 

diff --git a/...mc-regression/float19_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float19_.i b/...mc-regression/float19_true-unreach-call.i → ...loatingPoint/regression/c/cbmc_float19_.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_error(void);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
 
 
 

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float1_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float1_.i
@@ -0,0 +1,27 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+int main() {
+  double x;
+  int y;
+
+  x=2;
+  x-=0.6;
+  y=x;
+
+  if(!(y==1)) __VERIFIER_error();
+
+  x=2;
+  x-=0.4;
+  y=x;
+
+
+  if(!(y==1)) __VERIFIER_error();
+}
diff --git a/...ession/float20_true-unreach-call__Part1.i → ...gPoint/regression/c/cbmc_float20__Part1.i b/...ession/float20_true-unreach-call__Part1.i → ...gPoint/regression/c/cbmc_float20__Part1.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_assume(int);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_assume(int);
 extern void __VERIFIER_error(void);
 void bug (float min) {
   __VERIFIER_assume(min == 0x1.fffffep-105f);

diff --git a/...ession/float20_true-unreach-call__Part3.i → ...gPoint/regression/c/cbmc_float20__Part3.i b/...ession/float20_true-unreach-call__Part3.i → ...gPoint/regression/c/cbmc_float20__Part3.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_assume(int);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_assume(int);
 extern void __VERIFIER_error(void);
 void bug (float min) {
   __VERIFIER_assume(min == 0x1.fffffep-105f);

diff --git a/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float2_.i b/trunk/examples/programs/FloatingPoint/regression/c/cbmc_float2_.i
@@ -0,0 +1,31 @@
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_error(void);
+
+int main()
+{
+  float a;
+  double b;
+
+
+  a=1.25L;
+  if(!(a==1.25)) __VERIFIER_error();
+
+  b=1.250;
+  if(!(b==1.25)) __VERIFIER_error();
+
+
+  a=0.5e2;
+  if(!(a==50)) __VERIFIER_error();
+
+
+  a=0x1.4p+4;
+  if(!(a==20)) __VERIFIER_error();
+}
diff --git a/...ression/float4_true-unreach-call__PART1.i → ...ngPoint/regression/c/cbmc_float4__PART1.i b/...ression/float4_true-unreach-call__PART1.i → ...ngPoint/regression/c/cbmc_float4__PART1.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_assume(int);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_assume(int);
 
 
 

diff --git a/...ression/float4_true-unreach-call__PART2.i → ...ngPoint/regression/c/cbmc_float4__PART2.i b/...ression/float4_true-unreach-call__PART2.i → ...ngPoint/regression/c/cbmc_float4__PART2.i
@@ -1,4 +1,13 @@
-extern void __VERIFIER_assume(int);
+//#Safe
+
+/*
+ * Taken from CBMC's regression test suite
+ * (http://svn.cprover.org/svn/cbmc/trunk/regression/cbmc/).
+ *
+ * The overflow checks were omitted as these require more elaborate assertions.
+ */
+
+ extern void __VERIFIER_assume(int);