diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
index f7143072dadb3dbde1b7d5840e45bc85a7684888..2161d2fc0f7e7621343e918328102589aa8ca0bf 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
@@ -20,8 +20,6 @@ int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_assert(1,(char *)"Assertion",(char *)"main",(char *)"3 != 1.5",12);
- /*@ assert 3 ≢ 1.5; */ ;
{
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
@@ -41,7 +39,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",13);
+ (char *)"3 == 1.5 + 1.5",12);
__gmpq_clear(__gen_e_acsl_);
__gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl__3);
@@ -56,12 +54,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",14);
+ (char *)"main",(char *)"0.1 == 0.1",13);
__gmpq_clear(__gen_e_acsl__4);
}
/*@ assert 0.1 ≡ 0.1; */ ;
__e_acsl_assert(1,(char *)"Assertion",(char *)"main",
- (char *)"(double)1.0 == 1.0",15);
+ (char *)"(double)1.0 == 1.0",14);
/*@ assert (double)1.0 ≡ 1.0; */ ;
{
__e_acsl_mpq_t __gen_e_acsl__5;
@@ -77,7 +75,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",16);
+ (char *)"(double)0.1 != 0.1",15);
__gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl__7);
}
@@ -96,7 +94,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",17);
+ (char *)"(float)0.1 != (double)0.1",16);
__gmpq_clear(__gen_e_acsl__8);
}
/*@ assert (float)0.1 ≢ (double)0.1; */ ;
@@ -125,7 +123,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",18);
+ (char *)"main",(char *)"(double)1.1 != 1 + 0.1",17);
__gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__14);
@@ -160,7 +158,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",19);
+ (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",18);
__gmpq_clear(__gen_e_acsl__16);
__gmpq_clear(__gen_e_acsl__17);
__gmpq_clear(__gen_e_acsl_add_3);
@@ -191,7 +189,7 @@ 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",23);
+ (char *)"main",(char *)"sum != x * y",22);
__gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__20);
__gmpq_clear(__gen_e_acsl_mul);
@@ -219,7 +217,7 @@ int main(void)
__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_ne_4 != 0,(char *)"Assertion",
- (char *)"main",(char *)"1.1d != 1 + 0.1",30);
+ (char *)"main",(char *)"1.1d != 1 + 0.1",29);
__gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl__23);
__gmpq_clear(__gen_e_acsl_add_4);
diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
index a6a2923fc7d78b732768d31af599c9bae4a98cc8..6b6e958fe3307d88f08470895bdaf3de1960c169 100644
--- a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
@@ -1,45 +1,45 @@
-[kernel:parser:decimal-float] tests/arith/rationals.c:20: Warning:
+[kernel:parser:decimal-float] tests/arith/rationals.c:19: 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:17: Warning:
+[e-acsl] tests/arith/rationals.c:16: 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:13: Warning:
+[eva:alarm] tests/arith/rationals.c:12: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:14: 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:16: Warning:
+[eva:alarm] tests/arith/rationals.c:13: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:15: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/arith/rationals.c:16: Warning:
+[eva:alarm] tests/arith/rationals.c:15: 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:17: Warning:
+[eva:alarm] tests/arith/rationals.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:16: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/arith/rationals.c:17: Warning:
+[eva:alarm] tests/arith/rationals.c:16: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/arith/rationals.c:17: Warning:
+[eva:alarm] tests/arith/rationals.c:16: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/arith/rationals.c:17: Warning:
+[eva:alarm] tests/arith/rationals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:18: Warning:
+[eva:alarm] tests/arith/rationals.c:17: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
+[eva:alarm] tests/arith/rationals.c:17: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/rationals.c:17: Warning: assertion got status unknown.
[eva:alarm] tests/arith/rationals.c:18: 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:19: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:19: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/rationals.c:23: Warning:
+[eva:alarm] tests/arith/rationals.c:22: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:4: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/arith/rationals.c:4: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:30: Warning:
+[eva:alarm] tests/arith/rationals.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/rationals.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:29: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/rationals.c b/src/plugins/e-acsl/tests/arith/rationals.c
index 84c8b0949b4d44178f43101ad840b05ad734d50e..18ed5111f7089b4cb079af9d45d206907818ee31 100644
--- a/src/plugins/e-acsl/tests/arith/rationals.c
+++ b/src/plugins/e-acsl/tests/arith/rationals.c
@@ -9,7 +9,6 @@ double avg(double a, double b) {
}
int main(void) {
- /*@ assert 3 != 1.5; */ ;
/*@ assert 3 == 1.5 + 1.5; */ ;
/*@ assert 0.1 == 0.1; */ ;
/*@ assert (double)1.0 == 1.0; */ ;