From c1ffa08a3c3cd63e66f3748f1974c743545ab511 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 27 Aug 2019 15:06:56 +0200
Subject: [PATCH] [typing] improve precision for floats
---
src/plugins/e-acsl/interval.ml | 34 ++-
src/plugins/e-acsl/tests/gmp/functions.c | 5 +-
.../tests/gmp/oracle/functions.0.res.oracle | 10 +
.../tests/gmp/oracle/functions.1.res.oracle | 10 +
.../e-acsl/tests/gmp/oracle/gen_functions.c | 31 +++
.../e-acsl/tests/gmp/oracle/gen_functions2.c | 32 +++
.../e-acsl/tests/gmp/oracle/gen_reals.c | 259 +++++++++---------
.../e-acsl/tests/gmp/oracle/gen_reals2.c | 259 +++++++++---------
.../tests/gmp/oracle/reals.0.res.oracle | 18 +-
.../tests/gmp/oracle/reals.1.res.oracle | 18 +-
src/plugins/e-acsl/translate.ml | 3 +-
src/plugins/e-acsl/typing.ml | 6 +-
12 files changed, 383 insertions(+), 302 deletions(-)
diff --git a/src/plugins/e-acsl/interval.ml b/src/plugins/e-acsl/interval.ml
index 3aab01f01d3..4bf408a33b6 100644
--- a/src/plugins/e-acsl/interval.ml
+++ b/src/plugins/e-acsl/interval.ml
@@ -120,14 +120,42 @@ let lift_unop f = function
| Rational | Real | Nan as i -> i
let lift_binop ~safe_float f i1 i2 = match i1, i2 with
+ | Ival iv, i when Ival.is_bottom iv -> i
+ | i, Ival iv when Ival.is_bottom iv -> i
| Ival i1, Ival i2 ->
Ival (f i1 i2)
| Float(k1, _), Float(k2, _) when safe_float ->
let k = if Stdlib.compare k1 k2 >= 0 then k1 else k2 in
Float(k, None (* lost value, if any before *))
+ | Ival iv, Float(k, _)
+ | Float(k, _), Ival iv ->
+ if safe_float
+ then
+ match Ival.min_and_max iv with
+ | None, None ->
+ (* unbounded integers *)
+ Rational
+ | Some min, Some max ->
+ (* if the interval of integers fits into the float types, then return
+ this float type; otherwise return Rational *)
+ (try
+ let to_float n = Int64.to_float (Integer.to_int64 n) in
+ let mini, maxi = to_float min, to_float max in
+ let minf, maxf = match k with
+ | FFloat ->
+ Floating_point.most_negative_single_precision_float,
+ Floating_point.max_single_precision_float
+ | FDouble -> -. Float.max_float, Float.max_float
+ | FLongDouble -> raise Exit
+ in
+ if mini >= minf && maxi <= maxf then Float(k, None) else Rational
+ with Z.Overflow | Exit ->
+ Rational)
+ | None, Some _ | Some _, None ->
+ assert false
+ else Rational (* sound over-approximation *)
| (Ival _ | Float _ | Rational), (Float _ | Rational)
- | (Float _ | Rational), Ival _ ->
- (* any binary operator over a float or a rational generates a rational *)
+ | Rational, Ival _ ->
Rational
| (Ival _ | Float _ | Rational | Real), Real
| Real, (Ival _ | Float _ | Rational) ->
@@ -336,7 +364,7 @@ end = struct
let (_, p as named_p) = extract_profile ~infer old_profile t in
try
let old_i = LF.Hashtbl.find named_profiles named_p in
- if is_included i old_i then true, p, old_i
+ if is_included i old_i then true, p, old_i (* fixpoint reached *)
else begin
let j = join i old_i in
LF.Hashtbl.replace named_profiles named_p j;
diff --git a/src/plugins/e-acsl/tests/gmp/functions.c b/src/plugins/e-acsl/tests/gmp/functions.c
index 80f796bad6a..9d0bc001ab6 100644
--- a/src/plugins/e-acsl/tests/gmp/functions.c
+++ b/src/plugins/e-acsl/tests/gmp/functions.c
@@ -64,9 +64,10 @@ int main (void) {
k(9);
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */ ;
+
// not yet supported
- /* double d = 2.0; */
- /* /\*@ assert f2(d) > 0; *\/ ; */
/* /\*@ assert p_notyet(27); *\/ ; */
/* /\*@ assert f_notyet(27) == 27; *\/ ; */
}
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
index b922d39b016..f20e6ae071a 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
@@ -28,4 +28,14 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/functions.c:49: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpq_init
+[eva] using specification for function __gmpq_set_str
+[eva] using specification for function __gmpq_set_d
+[eva] using specification for function __gmpq_div
+[eva] using specification for function __gmpq_get_d
+[eva] using specification for function __gmpq_clear
+[eva:alarm] tests/gmp/functions.c:68: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__10);
+[eva:alarm] tests/gmp/functions.c:68: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
index 6a88f942fbc..f284f855063 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
+++ b/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
@@ -47,4 +47,14 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/gmp/functions.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpq_init
+[eva] using specification for function __gmpq_set_str
+[eva] using specification for function __gmpq_set_d
+[eva] using specification for function __gmpq_div
+[eva] using specification for function __gmpq_get_d
+[eva] using specification for function __gmpq_clear
+[eva:alarm] tests/gmp/functions.c:68: Warning:
+ non-finite double value. assert \is_finite(__gen_e_acsl__15);
+[eva:alarm] tests/gmp/functions.c:68: Warning:
+ function __e_acsl_assert: precondition got status unknown.
[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
index c71d46e5640..7863ef08ac2 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
@@ -74,6 +74,8 @@ int glob = 5;
*/
/*@ logic double f2(double x) = (double)(1 / x);
*/
+double __gen_e_acsl_f2(double x);
+
/*@ predicate p_notyet{L}(ℤ x) = x > 0;
*/
/*@ logic ℤ f_notyet{L}(ℤ x) = x;
@@ -203,6 +205,14 @@ int main(void)
(char *)"main",(char *)"t2(t1(m)) == 17",63);
}
__gen_e_acsl_k(9);
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */
+ {
+ double __gen_e_acsl_f2_2;
+ __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
+ __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,(char *)"Assertion",
+ (char *)"main",(char *)"f2(d) > 0",68);
+ }
__retres = 0;
return __retres;
}
@@ -230,6 +240,27 @@ int __gen_e_acsl_g_hidden(int x)
return x;
}
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__8;
+ __e_acsl_mpq_t __gen_e_acsl__9;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__10;
+ __gmpq_init(__gen_e_acsl__8);
+ __gmpq_set_str(__gen_e_acsl__8,"1",10);
+ __gmpq_init(__gen_e_acsl__9);
+ __gmpq_set_d(__gen_e_acsl__9,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,(__e_acsl_mpq_struct const *)(__gen_e_acsl__8),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__9));
+ __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__8);
+ __gmpq_clear(__gen_e_acsl__9);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
+ return __gen_e_acsl__10;
+}
+
int __gen_e_acsl_g(int x)
{
int __gen_e_acsl_g_hidden_2;
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
index 0feabbd93d9..7cf1bcc8904 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
@@ -72,6 +72,8 @@ int glob = 5;
*/
/*@ logic double f2(double x) = (double)(1 / x);
*/
+double __gen_e_acsl_f2(double x);
+
/*@ predicate p_notyet{L}(ℤ x) = x > 0;
*/
/*@ logic ℤ f_notyet{L}(ℤ x) = x;
@@ -249,6 +251,14 @@ int main(void)
__gmpz_clear(__gen_e_acsl__12);
}
__gen_e_acsl_k(9);
+ double d = 2.0;
+ /*@ assert f2(d) > 0; */
+ {
+ double __gen_e_acsl_f2_2;
+ __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
+ __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,(char *)"Assertion",
+ (char *)"main",(char *)"f2(d) > 0",68);
+ }
__retres = 0;
return __retres;
}
@@ -276,6 +286,28 @@ int __gen_e_acsl_g_hidden(int x)
return x;
}
+double __gen_e_acsl_f2(double x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__13;
+ __e_acsl_mpq_t __gen_e_acsl__14;
+ __e_acsl_mpq_t __gen_e_acsl_div;
+ double __gen_e_acsl__15;
+ __gmpq_init(__gen_e_acsl__13);
+ __gmpq_set_str(__gen_e_acsl__13,"1",10);
+ __gmpq_init(__gen_e_acsl__14);
+ __gmpq_set_d(__gen_e_acsl__14,x);
+ __gmpq_init(__gen_e_acsl_div);
+ __gmpq_div(__gen_e_acsl_div,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+ __gmpq_clear(__gen_e_acsl__13);
+ __gmpq_clear(__gen_e_acsl__14);
+ __gmpq_clear(__gen_e_acsl_div);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
+ return __gen_e_acsl__15;
+}
+
int __gen_e_acsl_g(int x)
{
int __gen_e_acsl_g_hidden_2;
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 2b998ee6660..7e0d70df561 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
@@ -21,166 +21,153 @@ int main(void)
int __retres;
__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);
+ /*@ assert 3 ≡ 1.5 + 1.5; */
{
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
- int __gen_e_acsl_ne;
+ __e_acsl_mpq_t __gen_e_acsl__3;
+ __e_acsl_mpq_t __gen_e_acsl_add;
+ int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"3",10);
__gmpq_init(__gen_e_acsl__2);
__gmpq_set_d(__gen_e_acsl__2,1.5);
- __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"3 != 1.5",14);
- __gmpq_clear(__gen_e_acsl_);
- __gmpq_clear(__gen_e_acsl__2);
- }
- /*@ assert 3 ≡ 1.5 + 1.5; */
- {
- __e_acsl_mpq_t __gen_e_acsl__3;
- __e_acsl_mpq_t __gen_e_acsl__4;
- __e_acsl_mpq_t __gen_e_acsl__5;
- __e_acsl_mpq_t __gen_e_acsl_add;
- int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_str(__gen_e_acsl__3,"3",10);
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_d(__gen_e_acsl__4,1.5);
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_d(__gen_e_acsl__5,1.5);
+ __gmpq_set_d(__gen_e_acsl__3,1.5);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
- __gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
+ __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);
+ __gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl__3);
- __gmpq_clear(__gen_e_acsl__4);
- __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_add);
}
/*@ assert 0.1 ≡ 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__6;
+ __e_acsl_mpq_t __gen_e_acsl__4;
int __gen_e_acsl_eq_2;
- __gmpq_init(__gen_e_acsl__6);
- __gmpq_set_str(__gen_e_acsl__6,"01/10",10);
- __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_str(__gen_e_acsl__4,"01/10",10);
+ __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);
- __gmpq_clear(__gen_e_acsl__6);
+ __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);
/*@ assert (double)0.1 ≢ 0.1; */
{
+ __e_acsl_mpq_t __gen_e_acsl__5;
+ double __gen_e_acsl__6;
__e_acsl_mpq_t __gen_e_acsl__7;
- double __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
- int __gen_e_acsl_ne_2;
+ int __gen_e_acsl_ne;
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_str(__gen_e_acsl__5,"01/10",10);
+ __gen_e_acsl__6 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gmpq_init(__gen_e_acsl__7);
- __gmpq_set_str(__gen_e_acsl__7,"01/10",10);
- __gen_e_acsl__8 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
- __gmpq_init(__gen_e_acsl__9);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__8); */
- __gmpq_set_d(__gen_e_acsl__9,__gen_e_acsl__8);
- __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",18);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__6); */
+ __gmpq_set_d(__gen_e_acsl__7,__gen_e_acsl__6);
+ __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);
+ __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl__7);
- __gmpq_clear(__gen_e_acsl__9);
}
/*@ assert (float)0.1 ≢ (double)0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__10;
- double __gen_e_acsl__11;
- double __gen_e_acsl__12;
- __gmpq_init(__gen_e_acsl__10);
- __gmpq_set_str(__gen_e_acsl__10,"01/10",10);
- __gen_e_acsl__11 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__11); */
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
- /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__11);
+ __e_acsl_mpq_t __gen_e_acsl__8;
+ double __gen_e_acsl__9;
+ double __gen_e_acsl__10;
+ __gmpq_init(__gen_e_acsl__8);
+ __gmpq_set_str(__gen_e_acsl__8,"01/10",10);
+ __gen_e_acsl__9 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__9); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__9);
*/
- __e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
+ __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);
- __gmpq_clear(__gen_e_acsl__10);
+ __gmpq_clear(__gen_e_acsl__8);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
{
+ __e_acsl_mpq_t __gen_e_acsl__11;
+ double __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl__13;
- double __gen_e_acsl__14;
- __e_acsl_mpq_t __gen_e_acsl__15;
- __e_acsl_mpq_t __gen_e_acsl__16;
+ __e_acsl_mpq_t __gen_e_acsl__14;
__e_acsl_mpq_t __gen_e_acsl_add_2;
- __e_acsl_mpq_t __gen_e_acsl__17;
- int __gen_e_acsl_ne_3;
+ __e_acsl_mpq_t __gen_e_acsl__15;
+ int __gen_e_acsl_ne_2;
+ __gmpq_init(__gen_e_acsl__11);
+ __gmpq_set_str(__gen_e_acsl__11,"11/10",10);
+ __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
__gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"11/10",10);
- __gen_e_acsl__14 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
- __gmpq_init(__gen_e_acsl__15);
- __gmpq_set_str(__gen_e_acsl__15,"1",10);
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_str(__gen_e_acsl__16,"01/10",10);
+ __gmpq_set_str(__gen_e_acsl__13,"1",10);
+ __gmpq_init(__gen_e_acsl__14);
+ __gmpq_set_str(__gen_e_acsl__14,"01/10",10);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__16));
- __gmpq_init(__gen_e_acsl__17);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__14); */
- __gmpq_set_d(__gen_e_acsl__17,__gen_e_acsl__14);
- __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ __gmpq_init(__gen_e_acsl__15);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
+ __gmpq_set_d(__gen_e_acsl__15,__gen_e_acsl__12);
+ __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_3 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
+ __gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__15);
- __gmpq_clear(__gen_e_acsl__16);
+ __gmpq_clear(__gen_e_acsl__14);
__gmpq_clear(__gen_e_acsl_add_2);
- __gmpq_clear(__gen_e_acsl__17);
+ __gmpq_clear(__gen_e_acsl__15);
}
/*@ assert 1 + 0.1 ≡ 2 - 0.9; */
{
+ __e_acsl_mpq_t __gen_e_acsl__16;
+ __e_acsl_mpq_t __gen_e_acsl__17;
+ __e_acsl_mpq_t __gen_e_acsl_add_3;
__e_acsl_mpq_t __gen_e_acsl__18;
__e_acsl_mpq_t __gen_e_acsl__19;
- __e_acsl_mpq_t __gen_e_acsl_add_3;
- __e_acsl_mpq_t __gen_e_acsl__20;
- __e_acsl_mpq_t __gen_e_acsl__21;
__e_acsl_mpq_t __gen_e_acsl_sub;
int __gen_e_acsl_eq_3;
- __gmpq_init(__gen_e_acsl__18);
- __gmpq_set_str(__gen_e_acsl__18,"1",10);
- __gmpq_init(__gen_e_acsl__19);
- __gmpq_set_str(__gen_e_acsl__19,"01/10",10);
+ __gmpq_init(__gen_e_acsl__16);
+ __gmpq_set_str(__gen_e_acsl__16,"1",10);
+ __gmpq_init(__gen_e_acsl__17);
+ __gmpq_set_str(__gen_e_acsl__17,"01/10",10);
__gmpq_init(__gen_e_acsl_add_3);
__gmpq_add(__gen_e_acsl_add_3,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_str(__gen_e_acsl__20,"2",10);
- __gmpq_init(__gen_e_acsl__21);
- __gmpq_set_str(__gen_e_acsl__21,"09/10",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__17));
+ __gmpq_init(__gen_e_acsl__18);
+ __gmpq_set_str(__gen_e_acsl__18,"2",10);
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_str(__gen_e_acsl__19,"09/10",10);
__gmpq_init(__gen_e_acsl_sub);
__gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__21));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
__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);
+ __gmpq_clear(__gen_e_acsl__16);
+ __gmpq_clear(__gen_e_acsl__17);
+ __gmpq_clear(__gen_e_acsl_add_3);
__gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl__19);
- __gmpq_clear(__gen_e_acsl_add_3);
- __gmpq_clear(__gen_e_acsl__20);
- __gmpq_clear(__gen_e_acsl__21);
__gmpq_clear(__gen_e_acsl_sub);
}
float x = 0.2f;
@@ -189,84 +176,84 @@ int main(void)
/*@ assert sum ≢ x * y; */
{
__e_acsl_mpq_t __gen_e_acsl_y;
- __e_acsl_mpq_t __gen_e_acsl__22;
+ __e_acsl_mpq_t __gen_e_acsl__20;
__e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__23;
- int __gen_e_acsl_ne_4;
+ __e_acsl_mpq_t __gen_e_acsl__21;
+ int __gen_e_acsl_ne_3;
__gmpq_init(__gen_e_acsl_y);
__gmpq_set_d(__gen_e_acsl_y,(double)y);
- __gmpq_init(__gen_e_acsl__22);
- __gmpq_set_d(__gen_e_acsl__22,(double)x);
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_d(__gen_e_acsl__20,(double)x);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gmpq_init(__gen_e_acsl__23);
- __gmpq_set_d(__gen_e_acsl__23,(double)sum);
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
+ __gmpq_init(__gen_e_acsl__21);
+ __gmpq_set_d(__gen_e_acsl__21,(double)sum);
+ __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_4 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",25);
__gmpq_clear(__gen_e_acsl_y);
- __gmpq_clear(__gen_e_acsl__22);
+ __gmpq_clear(__gen_e_acsl__20);
__gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__23);
+ __gmpq_clear(__gen_e_acsl__21);
}
/*@ assert \let n = 1; 4 ≡ n + 3.0; */
{
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__25;
- __e_acsl_mpq_t __gen_e_acsl__26;
__e_acsl_mpq_t __gen_e_acsl_add_4;
int __gen_e_acsl_eq_4;
__gen_e_acsl_n = 1;
+ __gmpq_init(__gen_e_acsl__22);
+ __gmpq_set_str(__gen_e_acsl__22,"4",10);
+ __gmpq_init(__gen_e_acsl__23);
+ __gmpq_set_d(__gen_e_acsl__23,3.);
__gmpq_init(__gen_e_acsl__24);
- __gmpq_set_str(__gen_e_acsl__24,"4",10);
- __gmpq_init(__gen_e_acsl__25);
- __gmpq_set_d(__gen_e_acsl__25,3.);
- __gmpq_init(__gen_e_acsl__26);
- __gmpq_set_si(__gen_e_acsl__26,(long)__gen_e_acsl_n);
+ __gmpq_set_si(__gen_e_acsl__24,(long)__gen_e_acsl_n);
__gmpq_init(__gen_e_acsl_add_4);
__gmpq_add(__gen_e_acsl_add_4,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__26),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__25));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__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),
(__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);
+ __gmpq_clear(__gen_e_acsl__22);
+ __gmpq_clear(__gen_e_acsl__23);
__gmpq_clear(__gen_e_acsl__24);
- __gmpq_clear(__gen_e_acsl__25);
- __gmpq_clear(__gen_e_acsl__26);
__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__27;
- __e_acsl_mpq_t __gen_e_acsl__28;
+ __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__29;
- int __gen_e_acsl_ne_5;
- __gmpq_init(__gen_e_acsl__27);
- __gmpq_set_str(__gen_e_acsl__27,"1",10);
- __gmpq_init(__gen_e_acsl__28);
- __gmpq_set_str(__gen_e_acsl__28,"01/10",10);
+ __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__27),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__28));
- __gmpq_init(__gen_e_acsl__29);
- __gmpq_set_d(__gen_e_acsl__29,1.1);
- __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
+ (__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_5 != 0,(char *)"Assertion",
+ __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__27);
- __gmpq_clear(__gen_e_acsl__28);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
__gmpq_clear(__gen_e_acsl_add_5);
- __gmpq_clear(__gen_e_acsl__29);
+ __gmpq_clear(__gen_e_acsl__27);
}
__retres = 0;
return __retres;
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 2b998ee6660..7e0d70df561 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
@@ -21,166 +21,153 @@ int main(void)
int __retres;
__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);
+ /*@ assert 3 ≡ 1.5 + 1.5; */
{
__e_acsl_mpq_t __gen_e_acsl_;
__e_acsl_mpq_t __gen_e_acsl__2;
- int __gen_e_acsl_ne;
+ __e_acsl_mpq_t __gen_e_acsl__3;
+ __e_acsl_mpq_t __gen_e_acsl_add;
+ int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl_);
__gmpq_set_str(__gen_e_acsl_,"3",10);
__gmpq_init(__gen_e_acsl__2);
__gmpq_set_d(__gen_e_acsl__2,1.5);
- __gen_e_acsl_ne = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
- __e_acsl_assert(__gen_e_acsl_ne != 0,(char *)"Assertion",(char *)"main",
- (char *)"3 != 1.5",14);
- __gmpq_clear(__gen_e_acsl_);
- __gmpq_clear(__gen_e_acsl__2);
- }
- /*@ assert 3 ≡ 1.5 + 1.5; */
- {
- __e_acsl_mpq_t __gen_e_acsl__3;
- __e_acsl_mpq_t __gen_e_acsl__4;
- __e_acsl_mpq_t __gen_e_acsl__5;
- __e_acsl_mpq_t __gen_e_acsl_add;
- int __gen_e_acsl_eq;
__gmpq_init(__gen_e_acsl__3);
- __gmpq_set_str(__gen_e_acsl__3,"3",10);
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_d(__gen_e_acsl__4,1.5);
- __gmpq_init(__gen_e_acsl__5);
- __gmpq_set_d(__gen_e_acsl__5,1.5);
+ __gmpq_set_d(__gen_e_acsl__3,1.5);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
- __gen_e_acsl_eq = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__3),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
+ __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);
+ __gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl__3);
- __gmpq_clear(__gen_e_acsl__4);
- __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl_add);
}
/*@ assert 0.1 ≡ 0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__6;
+ __e_acsl_mpq_t __gen_e_acsl__4;
int __gen_e_acsl_eq_2;
- __gmpq_init(__gen_e_acsl__6);
- __gmpq_set_str(__gen_e_acsl__6,"01/10",10);
- __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__6),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__6));
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_str(__gen_e_acsl__4,"01/10",10);
+ __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);
- __gmpq_clear(__gen_e_acsl__6);
+ __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);
/*@ assert (double)0.1 ≢ 0.1; */
{
+ __e_acsl_mpq_t __gen_e_acsl__5;
+ double __gen_e_acsl__6;
__e_acsl_mpq_t __gen_e_acsl__7;
- double __gen_e_acsl__8;
- __e_acsl_mpq_t __gen_e_acsl__9;
- int __gen_e_acsl_ne_2;
+ int __gen_e_acsl_ne;
+ __gmpq_init(__gen_e_acsl__5);
+ __gmpq_set_str(__gen_e_acsl__5,"01/10",10);
+ __gen_e_acsl__6 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__5));
__gmpq_init(__gen_e_acsl__7);
- __gmpq_set_str(__gen_e_acsl__7,"01/10",10);
- __gen_e_acsl__8 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__7));
- __gmpq_init(__gen_e_acsl__9);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__8); */
- __gmpq_set_d(__gen_e_acsl__9,__gen_e_acsl__8);
- __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",18);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__6); */
+ __gmpq_set_d(__gen_e_acsl__7,__gen_e_acsl__6);
+ __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);
+ __gmpq_clear(__gen_e_acsl__5);
__gmpq_clear(__gen_e_acsl__7);
- __gmpq_clear(__gen_e_acsl__9);
}
/*@ assert (float)0.1 ≢ (double)0.1; */
{
- __e_acsl_mpq_t __gen_e_acsl__10;
- double __gen_e_acsl__11;
- double __gen_e_acsl__12;
- __gmpq_init(__gen_e_acsl__10);
- __gmpq_set_str(__gen_e_acsl__10,"01/10",10);
- __gen_e_acsl__11 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__10));
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__11); */
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
- /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__11);
+ __e_acsl_mpq_t __gen_e_acsl__8;
+ double __gen_e_acsl__9;
+ double __gen_e_acsl__10;
+ __gmpq_init(__gen_e_acsl__8);
+ __gmpq_set_str(__gen_e_acsl__8,"01/10",10);
+ __gen_e_acsl__9 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl__10 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__9); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__10); */
+ /*@ assert Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl__9);
*/
- __e_acsl_assert((double)((float)__gen_e_acsl__11) != __gen_e_acsl__12,
+ __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);
- __gmpq_clear(__gen_e_acsl__10);
+ __gmpq_clear(__gen_e_acsl__8);
}
/*@ assert (double)1.1 ≢ 1 + 0.1; */
{
+ __e_acsl_mpq_t __gen_e_acsl__11;
+ double __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl__13;
- double __gen_e_acsl__14;
- __e_acsl_mpq_t __gen_e_acsl__15;
- __e_acsl_mpq_t __gen_e_acsl__16;
+ __e_acsl_mpq_t __gen_e_acsl__14;
__e_acsl_mpq_t __gen_e_acsl_add_2;
- __e_acsl_mpq_t __gen_e_acsl__17;
- int __gen_e_acsl_ne_3;
+ __e_acsl_mpq_t __gen_e_acsl__15;
+ int __gen_e_acsl_ne_2;
+ __gmpq_init(__gen_e_acsl__11);
+ __gmpq_set_str(__gen_e_acsl__11,"11/10",10);
+ __gen_e_acsl__12 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
__gmpq_init(__gen_e_acsl__13);
- __gmpq_set_str(__gen_e_acsl__13,"11/10",10);
- __gen_e_acsl__14 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
- __gmpq_init(__gen_e_acsl__15);
- __gmpq_set_str(__gen_e_acsl__15,"1",10);
- __gmpq_init(__gen_e_acsl__16);
- __gmpq_set_str(__gen_e_acsl__16,"01/10",10);
+ __gmpq_set_str(__gen_e_acsl__13,"1",10);
+ __gmpq_init(__gen_e_acsl__14);
+ __gmpq_set_str(__gen_e_acsl__14,"01/10",10);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__15),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__16));
- __gmpq_init(__gen_e_acsl__17);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__14); */
- __gmpq_set_d(__gen_e_acsl__17,__gen_e_acsl__14);
- __gen_e_acsl_ne_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__17),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
+ __gmpq_init(__gen_e_acsl__15);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__12); */
+ __gmpq_set_d(__gen_e_acsl__15,__gen_e_acsl__12);
+ __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_3 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_2 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",20);
+ __gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__15);
- __gmpq_clear(__gen_e_acsl__16);
+ __gmpq_clear(__gen_e_acsl__14);
__gmpq_clear(__gen_e_acsl_add_2);
- __gmpq_clear(__gen_e_acsl__17);
+ __gmpq_clear(__gen_e_acsl__15);
}
/*@ assert 1 + 0.1 ≡ 2 - 0.9; */
{
+ __e_acsl_mpq_t __gen_e_acsl__16;
+ __e_acsl_mpq_t __gen_e_acsl__17;
+ __e_acsl_mpq_t __gen_e_acsl_add_3;
__e_acsl_mpq_t __gen_e_acsl__18;
__e_acsl_mpq_t __gen_e_acsl__19;
- __e_acsl_mpq_t __gen_e_acsl_add_3;
- __e_acsl_mpq_t __gen_e_acsl__20;
- __e_acsl_mpq_t __gen_e_acsl__21;
__e_acsl_mpq_t __gen_e_acsl_sub;
int __gen_e_acsl_eq_3;
- __gmpq_init(__gen_e_acsl__18);
- __gmpq_set_str(__gen_e_acsl__18,"1",10);
- __gmpq_init(__gen_e_acsl__19);
- __gmpq_set_str(__gen_e_acsl__19,"01/10",10);
+ __gmpq_init(__gen_e_acsl__16);
+ __gmpq_set_str(__gen_e_acsl__16,"1",10);
+ __gmpq_init(__gen_e_acsl__17);
+ __gmpq_set_str(__gen_e_acsl__17,"01/10",10);
__gmpq_init(__gen_e_acsl_add_3);
__gmpq_add(__gen_e_acsl_add_3,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_str(__gen_e_acsl__20,"2",10);
- __gmpq_init(__gen_e_acsl__21);
- __gmpq_set_str(__gen_e_acsl__21,"09/10",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__17));
+ __gmpq_init(__gen_e_acsl__18);
+ __gmpq_set_str(__gen_e_acsl__18,"2",10);
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_str(__gen_e_acsl__19,"09/10",10);
__gmpq_init(__gen_e_acsl_sub);
__gmpq_sub(__gen_e_acsl_sub,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__21));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__18),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19));
__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);
+ __gmpq_clear(__gen_e_acsl__16);
+ __gmpq_clear(__gen_e_acsl__17);
+ __gmpq_clear(__gen_e_acsl_add_3);
__gmpq_clear(__gen_e_acsl__18);
__gmpq_clear(__gen_e_acsl__19);
- __gmpq_clear(__gen_e_acsl_add_3);
- __gmpq_clear(__gen_e_acsl__20);
- __gmpq_clear(__gen_e_acsl__21);
__gmpq_clear(__gen_e_acsl_sub);
}
float x = 0.2f;
@@ -189,84 +176,84 @@ int main(void)
/*@ assert sum ≢ x * y; */
{
__e_acsl_mpq_t __gen_e_acsl_y;
- __e_acsl_mpq_t __gen_e_acsl__22;
+ __e_acsl_mpq_t __gen_e_acsl__20;
__e_acsl_mpq_t __gen_e_acsl_mul;
- __e_acsl_mpq_t __gen_e_acsl__23;
- int __gen_e_acsl_ne_4;
+ __e_acsl_mpq_t __gen_e_acsl__21;
+ int __gen_e_acsl_ne_3;
__gmpq_init(__gen_e_acsl_y);
__gmpq_set_d(__gen_e_acsl_y,(double)y);
- __gmpq_init(__gen_e_acsl__22);
- __gmpq_set_d(__gen_e_acsl__22,(double)x);
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_d(__gen_e_acsl__20,(double)x);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__22),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gmpq_init(__gen_e_acsl__23);
- __gmpq_set_d(__gen_e_acsl__23,(double)sum);
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
+ __gmpq_init(__gen_e_acsl__21);
+ __gmpq_set_d(__gen_e_acsl__21,(double)sum);
+ __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_4 != 0,(char *)"Assertion",
+ __e_acsl_assert(__gen_e_acsl_ne_3 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",25);
__gmpq_clear(__gen_e_acsl_y);
- __gmpq_clear(__gen_e_acsl__22);
+ __gmpq_clear(__gen_e_acsl__20);
__gmpq_clear(__gen_e_acsl_mul);
- __gmpq_clear(__gen_e_acsl__23);
+ __gmpq_clear(__gen_e_acsl__21);
}
/*@ assert \let n = 1; 4 ≡ n + 3.0; */
{
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__25;
- __e_acsl_mpq_t __gen_e_acsl__26;
__e_acsl_mpq_t __gen_e_acsl_add_4;
int __gen_e_acsl_eq_4;
__gen_e_acsl_n = 1;
+ __gmpq_init(__gen_e_acsl__22);
+ __gmpq_set_str(__gen_e_acsl__22,"4",10);
+ __gmpq_init(__gen_e_acsl__23);
+ __gmpq_set_d(__gen_e_acsl__23,3.);
__gmpq_init(__gen_e_acsl__24);
- __gmpq_set_str(__gen_e_acsl__24,"4",10);
- __gmpq_init(__gen_e_acsl__25);
- __gmpq_set_d(__gen_e_acsl__25,3.);
- __gmpq_init(__gen_e_acsl__26);
- __gmpq_set_si(__gen_e_acsl__26,(long)__gen_e_acsl_n);
+ __gmpq_set_si(__gen_e_acsl__24,(long)__gen_e_acsl_n);
__gmpq_init(__gen_e_acsl_add_4);
__gmpq_add(__gen_e_acsl_add_4,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__26),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__25));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__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),
(__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);
+ __gmpq_clear(__gen_e_acsl__22);
+ __gmpq_clear(__gen_e_acsl__23);
__gmpq_clear(__gen_e_acsl__24);
- __gmpq_clear(__gen_e_acsl__25);
- __gmpq_clear(__gen_e_acsl__26);
__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__27;
- __e_acsl_mpq_t __gen_e_acsl__28;
+ __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__29;
- int __gen_e_acsl_ne_5;
- __gmpq_init(__gen_e_acsl__27);
- __gmpq_set_str(__gen_e_acsl__27,"1",10);
- __gmpq_init(__gen_e_acsl__28);
- __gmpq_set_str(__gen_e_acsl__28,"01/10",10);
+ __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__27),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__28));
- __gmpq_init(__gen_e_acsl__29);
- __gmpq_set_d(__gen_e_acsl__29,1.1);
- __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__29),
+ (__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_5 != 0,(char *)"Assertion",
+ __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__27);
- __gmpq_clear(__gen_e_acsl__28);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
__gmpq_clear(__gen_e_acsl_add_5);
- __gmpq_clear(__gen_e_acsl__29);
+ __gmpq_clear(__gen_e_acsl__27);
}
__retres = 0;
return __retres;
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 5925779d7e0..2c4d33e93dd 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
@@ -19,37 +19,35 @@
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_sound_verdict ∈ [--..--]
[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_assert
[eva] using specification for function __gmpq_init
[eva] using specification for function __gmpq_set_str
[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/reals.c:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_clear
[eva] using specification for function __gmpq_add
+[eva] using specification for function __gmpq_cmp
[eva:alarm] tests/gmp/reals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpq_clear
[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:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__8);
+ non-finite double value. assert \is_finite(__gen_e_acsl__6);
[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);
+ non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__12);
+ non-finite double value. assert \is_finite(__gen_e_acsl__10);
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
[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:alarm] tests/gmp/reals.c:20: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__14);
+ non-finite double value. assert \is_finite(__gen_e_acsl__12);
[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.
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 5925779d7e0..2c4d33e93dd 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
@@ -19,37 +19,35 @@
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_sound_verdict ∈ [--..--]
[eva] using specification for function __e_acsl_memory_init
+[eva] using specification for function __e_acsl_assert
[eva] using specification for function __gmpq_init
[eva] using specification for function __gmpq_set_str
[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_cmp
-[eva] using specification for function __e_acsl_assert
-[eva:alarm] tests/gmp/reals.c:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_clear
[eva] using specification for function __gmpq_add
+[eva] using specification for function __gmpq_cmp
[eva:alarm] tests/gmp/reals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
+[eva] using specification for function __gmpq_clear
[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:18: Warning: assertion got status unknown.
[eva] using specification for function __gmpq_get_d
[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__8);
+ non-finite double value. assert \is_finite(__gen_e_acsl__6);
[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);
+ non-finite double value. assert \is_finite(__gen_e_acsl__9);
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__12);
+ non-finite double value. assert \is_finite(__gen_e_acsl__10);
[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl__11);
+ non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
[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:alarm] tests/gmp/reals.c:20: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__14);
+ non-finite double value. assert \is_finite(__gen_e_acsl__12);
[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.
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 82de0f17f9f..b58640843e4 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -156,7 +156,8 @@ let constant_to_exp ~loc t c =
| Typing.Gmpz ->
(* too large integer *)
Cil.mkString ~loc (Integer.to_string n), Str_Z
- | Typing.C_float _fkind -> assert false (* TODO RATIONAL *)
+ | Typing.C_float fkind ->
+ Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64 n)), C_number
| Typing.C_integer kind ->
let cast = Typing.get_cast t in
match cast, kind with
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 774e0c22d3f..8abc13fd1cb 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -243,10 +243,8 @@ let ty_of_interv ?ctx = function
(* return [ctx] type for types smaller than int to prevent superfluous
casts in the generated code *)
if Cil.intTypeIncluded kind ik then ctx else C_integer kind
- | Some (C_float _ | Rational) ->
- Rational
- | Some Real ->
- Real)
+ | Some (C_float _ | Rational | Real as ty) ->
+ ty)
with Cil.Not_representable ->
match ctx with
| None | Some(C_integer _ | Gmpz | Nan) -> Gmpz
--
GitLab