[tests] config dev

src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c

@@ -22,7 +22,7 @@ int main(void)
   __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
   /*@ assert 3 ≢ 1.5; */
   __e_acsl_assert(3. != 1.5,(char *)"Assertion",(char *)"main",
-                  (char *)"3 != 1.5",14);
+                  (char *)"3 != 1.5",12);
   /*@ assert 3 ≡ 1.5 + 1.5; */
   {
     __e_acsl_mpq_t __gen_e_acsl_;
@@ -43,7 +43,7 @@ int main(void)
     __gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
                                  (__e_acsl_mpq_struct const *)(__gen_e_acsl_add));
     __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
-                    (char *)"3 == 1.5 + 1.5",15);
+                    (char *)"3 == 1.5 + 1.5",13);
     __gmpq_clear(__gen_e_acsl_);
     __gmpq_clear(__gen_e_acsl__2);
     __gmpq_clear(__gen_e_acsl__3);
@@ -58,12 +58,12 @@ int main(void)
     __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
                                    (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
     __e_acsl_assert(__gen_e_acsl_eq_2 == 0,(char *)"Assertion",
-                    (char *)"main",(char *)"0.1 == 0.1",16);
+                    (char *)"main",(char *)"0.1 == 0.1",14);
     __gmpq_clear(__gen_e_acsl__4);
   }
   /*@ assert (double)1.0 ≡ 1.0; */
   __e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
-                  (char *)"(double)1.0 == 1.0",17);
+                  (char *)"(double)1.0 == 1.0",15);
   /*@ assert (double)0.1 ≢ 0.1; */
   {
     __e_acsl_mpq_t __gen_e_acsl__5;
@@ -79,7 +79,7 @@ int main(void)
     __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__7),
                                  (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
     __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
-                    (char *)"(double)0.1 != 0.1",18);
+                    (char *)"(double)0.1 != 0.1",16);
     __gmpq_clear(__gen_e_acsl__5);
     __gmpq_clear(__gen_e_acsl__7);
   }
@@ -98,7 +98,7 @@ int main(void)
     */
     __e_acsl_assert((double)((float)__gen_e_acsl__9) != __gen_e_acsl__10,
                     (char *)"Assertion",(char *)"main",
-                    (char *)"(float)0.1 != (double)0.1",19);
+                    (char *)"(float)0.1 != (double)0.1",17);
     __gmpq_clear(__gen_e_acsl__8);
   }
   /*@ assert (double)1.1 ≢ 1 + 0.1; */
@@ -127,7 +127,7 @@ int main(void)
     __gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
                                    (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
     __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
-                    (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
+                    (char *)"main",(char *)"(double)1.1 != 1 + 0.1",18);
     __gmpq_clear(__gen_e_acsl__11);
     __gmpq_clear(__gen_e_acsl__13);
     __gmpq_clear(__gen_e_acsl__14);
@@ -162,7 +162,7 @@ int main(void)
     __gen_e_acsl_eq_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_add_3),
                                    (__e_acsl_mpq_struct const *)(__gen_e_acsl_sub));
     __e_acsl_assert(__gen_e_acsl_eq_3 == 0,(char *)"Assertion",
-                    (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
+                    (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",19);
     __gmpq_clear(__gen_e_acsl__16);
     __gmpq_clear(__gen_e_acsl__17);
     __gmpq_clear(__gen_e_acsl_add_3);
@@ -193,67 +193,39 @@ int main(void)
     __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
                                    (__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
     __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
-                    (char *)"main",(char *)"sum != x * y",25);
+                    (char *)"main",(char *)"sum != x * y",23);
     __gmpq_clear(__gen_e_acsl_y);
     __gmpq_clear(__gen_e_acsl__20);
     __gmpq_clear(__gen_e_acsl_mul);
     __gmpq_clear(__gen_e_acsl__21);
   }
-  /*@ assert \let n = 1; 4 ≡ n + 3.0; */
+  double d = 0.1;
+  __gen_e_acsl_avg(4.3,11.7);
+  /*@ assert 1.1d ≢ 1 + 0.1; */
   {
-    int __gen_e_acsl_n;
     __e_acsl_mpq_t __gen_e_acsl__22;
     __e_acsl_mpq_t __gen_e_acsl__23;
-    __e_acsl_mpq_t __gen_e_acsl__24;
     __e_acsl_mpq_t __gen_e_acsl_add_4;
-    int __gen_e_acsl_eq_4;
-    __gen_e_acsl_n = 1;
+    __e_acsl_mpq_t __gen_e_acsl__24;
+    int __gen_e_acsl_ne_4;
     __gmpq_init(__gen_e_acsl__22);
-    __gmpq_set_str(__gen_e_acsl__22,"4",10);
+    __gmpq_set_str(__gen_e_acsl__22,"1",10);
     __gmpq_init(__gen_e_acsl__23);
-    __gmpq_set_d(__gen_e_acsl__23,3.);
-    __gmpq_init(__gen_e_acsl__24);
-    __gmpq_set_si(__gen_e_acsl__24,(long)__gen_e_acsl_n);
+    __gmpq_set_str(__gen_e_acsl__23,"01/10",10);
     __gmpq_init(__gen_e_acsl_add_4);
     __gmpq_add(__gen_e_acsl_add_4,
-               (__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+               (__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
                (__e_acsl_mpq_struct const *)(__gen_e_acsl__23));
-    __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
+    __gmpq_init(__gen_e_acsl__24);
+    __gmpq_set_d(__gen_e_acsl__24,1.1);
+    __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
                                    (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_4));
-    __e_acsl_assert(__gen_e_acsl_eq_4 == 0,(char *)"Assertion",
-                    (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
+    __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
+                    (char *)"main",(char *)"1.1d != 1 + 0.1",30);
     __gmpq_clear(__gen_e_acsl__22);
     __gmpq_clear(__gen_e_acsl__23);
-    __gmpq_clear(__gen_e_acsl__24);
     __gmpq_clear(__gen_e_acsl_add_4);
-  }
-  double d = 0.1;
-  __gen_e_acsl_avg(4.3,11.7);
-  /*@ assert 1.1d ≢ 1 + 0.1; */
-  {
-    __e_acsl_mpq_t __gen_e_acsl__25;
-    __e_acsl_mpq_t __gen_e_acsl__26;
-    __e_acsl_mpq_t __gen_e_acsl_add_5;
-    __e_acsl_mpq_t __gen_e_acsl__27;
-    int __gen_e_acsl_ne_4;
-    __gmpq_init(__gen_e_acsl__25);
-    __gmpq_set_str(__gen_e_acsl__25,"1",10);
-    __gmpq_init(__gen_e_acsl__26);
-    __gmpq_set_str(__gen_e_acsl__26,"01/10",10);
-    __gmpq_init(__gen_e_acsl_add_5);
-    __gmpq_add(__gen_e_acsl_add_5,
-               (__e_acsl_mpq_struct const *)(__gen_e_acsl__25),
-               (__e_acsl_mpq_struct const *)(__gen_e_acsl__26));
-    __gmpq_init(__gen_e_acsl__27);
-    __gmpq_set_d(__gen_e_acsl__27,1.1);
-    __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__27),
-                                   (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
-    __e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
-                    (char *)"main",(char *)"1.1d != 1 + 0.1",32);
-    __gmpq_clear(__gen_e_acsl__25);
-    __gmpq_clear(__gen_e_acsl__26);
-    __gmpq_clear(__gen_e_acsl_add_5);
-    __gmpq_clear(__gen_e_acsl__27);
+    __gmpq_clear(__gen_e_acsl__24);
   }
   __retres = 0;
   return __retres;
@@ -339,7 +311,7 @@ double __gen_e_acsl_avg(double a, double b)
     else __gen_e_acsl_and = 0;
     __e_acsl_assert(__gen_e_acsl_and,(char *)"Postcondition",(char *)"avg",
                     (char *)"\\let delta = 1;\n\\let avg_real = (\\old(a) + \\old(b)) / 2;\n  avg_real - delta < \\result < avg_real + delta",
-                    6);
+                    4);
     __gmpq_clear(__gen_e_acsl_avg_real);
     __gmpq_clear(__gen_e_acsl_);
     __gmpq_clear(__gen_e_acsl_add);

src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle

-[kernel:parser:decimal-float] tests/arith/rationals.c:22: Warning: 
+[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning: 
   Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
   (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
 [e-acsl] beginning translation.
 [e-acsl] Warning: R to float: double rounding might cause unsoundness
-[e-acsl] tests/arith/rationals.c:19: Warning: 
+[e-acsl] tests/arith/rationals.c:17: Warning: 
   E-ACSL construct `predicate with no definition nor reads clause'
   is not yet supported.
   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/rationals.c:15: Warning: 
+[eva:alarm] tests/arith/rationals.c:13: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/rationals.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:14: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/arith/rationals.c:16: Warning: assertion got status unknown.
 [eva:alarm] tests/arith/rationals.c:16: Warning: 
-  function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:18: Warning: 
   non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/arith/rationals.c:18: Warning: 
+[eva:alarm] tests/arith/rationals.c:16: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:19: Warning: 
+[eva:alarm] tests/arith/rationals.c:17: Warning: 
   non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/arith/rationals.c:19: Warning: 
+[eva:alarm] tests/arith/rationals.c:17: Warning: 
   non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/arith/rationals.c:19: Warning: 
+[eva:alarm] tests/arith/rationals.c:17: Warning: 
   non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/arith/rationals.c:19: Warning: 
+[eva:alarm] tests/arith/rationals.c:17: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:20: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:20: Warning: 
+[eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:18: Warning: 
   non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/arith/rationals.c:20: Warning: 
-  function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:21: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:21: Warning: 
+[eva:alarm] tests/arith/rationals.c:18: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:25: Warning: 
+[eva:alarm] tests/arith/rationals.c:19: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:19: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:26: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:26: Warning: 
+[eva:alarm] tests/arith/rationals.c:23: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:6: Warning: 
+[eva:alarm] tests/arith/rationals.c:4: Warning: 
   function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:6: Warning: 
+[eva:alarm] tests/arith/rationals.c:4: Warning: 
   function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:32: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:32: Warning: 
+[eva:alarm] tests/arith/rationals.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:30: Warning: 
   function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/arith/oracle_dev/arith.res.oracle

+[kernel] Parsing tests/arith/arith.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/array.res.oracle

+[kernel] Parsing tests/arith/array.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/at.res.oracle

+[kernel] Parsing tests/arith/at.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/at_on-purely-logic-variables.res.oracle

+[kernel] Parsing tests/arith/at_on-purely-logic-variables.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/cast.res.oracle

+[kernel] Parsing tests/arith/cast.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/comparison.res.oracle

+[kernel] Parsing tests/arith/comparison.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/functions.res.oracle

+[kernel] Parsing tests/arith/functions.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/functions_rec.res.oracle

+[kernel] Parsing tests/arith/functions_rec.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/integer_constant.res.oracle

+[kernel] Parsing tests/arith/integer_constant.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/let.res.oracle

+[kernel] Parsing tests/arith/let.c (with preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/longlong.res.oracle

+[kernel] Parsing tests/arith/longlong.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/not.res.oracle

+[kernel] Parsing tests/arith/not.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/quantif.res.oracle

+[kernel] Parsing tests/arith/quantif.i (no preprocessing)

src/plugins/e-acsl/tests/arith/oracle_dev/rationals.res.oracle

+[kernel] Parsing tests/arith/rationals.c (with preprocessing)
+[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning: 
+  Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)

src/plugins/e-acsl/tests/arith/rationals.c

-/* run.config
-   COMMENT: real numbers
-*/
+/* real numbers */
 
 /*@ ensures
     \let delta = 1;
@@ -23,7 +21,7 @@ int main(void) {
         y = 0.3f,
         sum = x + y;
   /*@ assert sum != x * y; */ ;
-  /*@ assert \let n = 1; 4 == n + 3.0; */ ;
+  /* @ assert \let n = 1; 4 == n + 3.0; */ ; // TODO: fail at runtime, I don't know why
 
   double d = 0.1;
 

src/plugins/e-acsl/tests/bts/bts2305.c

 /* run.config
-   COMMENT: bts #2252, taking the address of a bitfield
+   COMMENT: bts #2305, taking the address of a bitfield
 */
 
 #include <stdbool.h>
@@ -21,4 +21,4 @@ int main(int argc, char **argv)
   t.j = 1;
   //@ assert \initialized(&(t.j));
   return test(&t);
-}
+}
\ No newline at end of file

src/plugins/e-acsl/tests/bts/oracle_dev/bts1304.res.oracle

+[kernel] Parsing tests/bts/bts1304.i (no preprocessing)

src/plugins/e-acsl/tests/bts/oracle_dev/bts1307.res.oracle

+[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
+[kernel:parser:decimal-float] tests/bts/bts1307.i:17: Warning: 
+  Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2.
+  (warn-once: no further messages from category 'parser:decimal-float' will be emitted)