diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
index 3033a792d26c9d50af66c5fa15d517a101cb1fbe..2b998ee6660a3aea136f3271f2cfd409297e46e6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
@@ -74,6 +74,9 @@ int main(void)
(char *)"main",(char *)"0.1 == 0.1",16);
__gmpq_clear(__gen_e_acsl__6);
}
+ /*@ assert (double)1.0 ≡ 1.0; */
+ __e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
+ (char *)"(double)1.0 == 1.0",17);
/*@ assert (double)0.1 ≢ 0.1; */
{
__e_acsl_mpq_t __gen_e_acsl__7;
@@ -89,7 +92,7 @@ int main(void)
__gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(double)0.1 != 0.1",17);
+ (char *)"main",(char *)"(double)0.1 != 0.1",18);
__gmpq_clear(__gen_e_acsl__7);
__gmpq_clear(__gen_e_acsl__9);
}
@@ -108,7 +111,7 @@ int main(void)
*/
__e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
(char *)"Assertion",(char *)"main",
- (char *)"(float)0.1 != (double)0.1",18);
+ (char *)"(float)0.1 != (double)0.1",19);
__gmpq_clear(__gen_e_acsl__10);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
@@ -137,7 +140,7 @@ int main(void)
__gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(double)1.1 != 1 + 0.1",19);
+ (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
__gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__15);
__gmpq_clear(__gen_e_acsl__16);
@@ -172,7 +175,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",20);
+ (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
__gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl__19);
__gmpq_clear(__gen_e_acsl_add_3);
@@ -203,7 +206,7 @@ int main(void)
__gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
- (char *)"main",(char *)"sum != x * y",24);
+ (char *)"main",(char *)"sum != x * y",25);
__gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl_mul);
@@ -231,7 +234,7 @@ int main(void)
__gen_e_acsl_eq_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",25);
+ (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
__gmpq_clear(__gen_e_acsl__24);
__gmpq_clear(__gen_e_acsl__25);
__gmpq_clear(__gen_e_acsl__26);
@@ -259,7 +262,7 @@ int main(void)
__gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
__e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
- (char *)"main",(char *)"1.1d != 1 + 0.1",31);
+ (char *)"main",(char *)"1.1d != 1 + 0.1",32);
__gmpq_clear(__gen_e_acsl__27);
__gmpq_clear(__gen_e_acsl__28);
__gmpq_clear(__gen_e_acsl_add_5);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
index 3033a792d26c9d50af66c5fa15d517a101cb1fbe..2b998ee6660a3aea136f3271f2cfd409297e46e6 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
@@ -74,6 +74,9 @@ int main(void)
(char *)"main",(char *)"0.1 == 0.1",16);
__gmpq_clear(__gen_e_acsl__6);
}
+ /*@ assert (double)1.0 ≡ 1.0; */
+ __e_acsl_assert(1. == 1.,(char *)"Assertion",(char *)"main",
+ (char *)"(double)1.0 == 1.0",17);
/*@ assert (double)0.1 ≢ 0.1; */
{
__e_acsl_mpq_t __gen_e_acsl__7;
@@ -89,7 +92,7 @@ int main(void)
__gen_e_acsl_ne_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__9),
(__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(double)0.1 != 0.1",17);
+ (char *)"main",(char *)"(double)0.1 != 0.1",18);
__gmpq_clear(__gen_e_acsl__7);
__gmpq_clear(__gen_e_acsl__9);
}
@@ -108,7 +111,7 @@ int main(void)
*/
__e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
(char *)"Assertion",(char *)"main",
- (char *)"(float)0.1 != (double)0.1",18);
+ (char *)"(float)0.1 != (double)0.1",19);
__gmpq_clear(__gen_e_acsl__10);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
@@ -137,7 +140,7 @@ int main(void)
__gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
- (char *)"main",(char *)"(double)1.1 != 1 + 0.1",19);
+ (char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
__gmpq_clear(__gen_e_acsl__13);
__gmpq_clear(__gen_e_acsl__15);
__gmpq_clear(__gen_e_acsl__16);
@@ -172,7 +175,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",20);
+ (char *)"main",(char *)"1 + 0.1 == 2 - 0.9",21);
__gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl__19);
__gmpq_clear(__gen_e_acsl_add_3);
@@ -203,7 +206,7 @@ int main(void)
__gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
- (char *)"main",(char *)"sum != x * y",24);
+ (char *)"main",(char *)"sum != x * y",25);
__gmpq_clear(__gen_e_acsl_y);
__gmpq_clear(__gen_e_acsl__22);
__gmpq_clear(__gen_e_acsl_mul);
@@ -231,7 +234,7 @@ int main(void)
__gen_e_acsl_eq_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",25);
+ (char *)"main",(char *)"\\let n = 1; 4 == n + 3.0",26);
__gmpq_clear(__gen_e_acsl__24);
__gmpq_clear(__gen_e_acsl__25);
__gmpq_clear(__gen_e_acsl__26);
@@ -259,7 +262,7 @@ int main(void)
__gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
__e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
- (char *)"main",(char *)"1.1d != 1 + 0.1",31);
+ (char *)"main",(char *)"1.1d != 1 + 0.1",32);
__gmpq_clear(__gen_e_acsl__27);
__gmpq_clear(__gen_e_acsl__28);
__gmpq_clear(__gen_e_acsl_add_5);
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
index c17cb20a38b2b1165d3aab40dc144b871549f964..5925779d7e08a2dd08ec846f531a2d90250c5a3b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
@@ -1,9 +1,9 @@
-[kernel:parser:decimal-float] tests/gmp/reals.c:21: Warning:
+[kernel:parser:decimal-float] tests/gmp/reals.c:22: 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/gmp/reals.c:18: Warning:
+[e-acsl] tests/gmp/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
@@ -33,35 +33,35 @@
[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:17: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
-[eva:alarm] tests/gmp/reals.c:17: Warning:
+[eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__8);
-[eva:alarm] tests/gmp/reals.c:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__11);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
+[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__14);
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
-[eva] using specification for function __gmpq_sub
+[eva:alarm] tests/gmp/reals.c:20: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__14);
[eva:alarm] tests/gmp/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
+[eva] using specification for function __gmpq_sub
+[eva:alarm] tests/gmp/reals.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_mul
-[eva:alarm] tests/gmp/reals.c:24: Warning:
+[eva:alarm] tests/gmp/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_set_si
-[eva:alarm] tests/gmp/reals.c:25: Warning:
+[eva:alarm] tests/gmp/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_set
[eva] using specification for function __gmpq_div
@@ -69,7 +69,7 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:31: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:31: Warning:
+[eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
index c17cb20a38b2b1165d3aab40dc144b871549f964..5925779d7e08a2dd08ec846f531a2d90250c5a3b 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel:parser:decimal-float] tests/gmp/reals.c:21: Warning:
+[kernel:parser:decimal-float] tests/gmp/reals.c:22: 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/gmp/reals.c:18: Warning:
+[e-acsl] tests/gmp/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
@@ -33,35 +33,35 @@
[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:17: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
-[eva:alarm] tests/gmp/reals.c:17: Warning:
+[eva:alarm] tests/gmp/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__8);
-[eva:alarm] tests/gmp/reals.c:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:18: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__11);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
+[eva:alarm] tests/gmp/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:19: Warning: assertion got status unknown.
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__14);
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
[eva:alarm] tests/gmp/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
-[eva] using specification for function __gmpq_sub
+[eva:alarm] tests/gmp/reals.c:20: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__14);
[eva:alarm] tests/gmp/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
+[eva] using specification for function __gmpq_sub
+[eva:alarm] tests/gmp/reals.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_mul
-[eva:alarm] tests/gmp/reals.c:24: Warning:
+[eva:alarm] tests/gmp/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_set_si
-[eva:alarm] tests/gmp/reals.c:25: Warning:
+[eva:alarm] tests/gmp/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] using specification for function __gmpq_set
[eva] using specification for function __gmpq_div
@@ -69,7 +69,7 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:31: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:31: Warning:
+[eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/reals.c b/src/plugins/e-acsl/tests/gmp/reals.c
index d199b47504555a479b6268e2be5c6d64556f76ee..ba944cedc2ed59d19431ed9185d0a245187c8abe 100644
--- a/src/plugins/e-acsl/tests/gmp/reals.c
+++ b/src/plugins/e-acsl/tests/gmp/reals.c
@@ -14,6 +14,7 @@ int main(void) {
/*@ assert 3 != 1.5; */ ;
/*@ assert 3 == 1.5 + 1.5; */ ;
/*@ assert 0.1 == 0.1; */ ;
+ /*@ assert (double)1.0 == 1.0; */ ;
/*@ assert (double)0.1 != 0.1; */ ;
/*@ assert (float)0.1 != (double)0.1; */ ;
/*@ assert (double)1.1 != 1 + 0.1 ;*/ ;