diff --git a/src/plugins/e-acsl/real.ml b/src/plugins/e-acsl/real.ml
index 5a530410a0cee366f60372a7fc70a5adb3d3014f..8827392aaf1eeb7b0b69a137cde0ee25bb90347e 100644
--- a/src/plugins/e-acsl/real.ml
+++ b/src/plugins/e-acsl/real.ml
@@ -60,6 +60,11 @@ let mk_real ~loc ?name e env t_opt =
e, env
exception Not_a_decimal of string
+exception Is_a_float
+
+(* The possible float suffixes (ISO C 6.4.4.2) are lLfF.
+ dD is a GNU extension accepted by Frama-C (only!) in the logic *)
+let float_suffixes = [ 'f'; 'F'; 'l'; 'L'; 'd'; 'D' ]
(* Computes the fractional representation of a decimal number.
Does NOT perform reduction.
@@ -88,6 +93,10 @@ let decimal_to_fractional str =
Bytes.unsafe_set buf (i - 1) c;
Bytes.unsafe_set buf len' '0';
post str len buf (len' + 1) (i + 1)
+ | c when List.mem c float_suffixes ->
+ (* [JS] a suffix denoting a C type is possible *)
+ assert (i = len - 1);
+ raise Is_a_float
| _ ->
raise (Not_a_decimal str)
in
@@ -106,6 +115,10 @@ let decimal_to_fractional str =
| c when '0' <= c && c <= '9' ->
Bytes.unsafe_set buf i c;
pre str len buf (i + 1)
+ | c when List.mem c float_suffixes ->
+ (* [JS] a suffix denoting a C type is possible *)
+ assert (i = len - 1);
+ raise Is_a_float
| _ ->
raise (Not_a_decimal str)
in
@@ -115,7 +128,8 @@ let decimal_to_fractional str =
as the decimal one. *)
2 * strlen
in
- pre str strlen (Bytes.create buflen) 0
+ try pre str strlen (Bytes.create buflen) 0
+ with Is_a_float -> str (* just left it unchanged *)
(* ACSL considers strings written in decimal expansion to be reals.
Yet GMPQ considers them to be double:
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 6bba81c1a8918212a07a50ff815639fe1a6cfa5b..7627bd75e465e994363437329d9248bf68129f77 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
@@ -1,6 +1,8 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
/*@ ensures \let delta = 1;
\let avg_real = (\old(a) + \old(b)) / 2;
avg_real - delta < \result < avg_real + delta;
@@ -91,20 +93,20 @@ int main(void)
{
__e_acsl_mpq_t __gen_e_acsl__8;
double __gen_e_acsl_cast_2;
- __e_acsl_mpq_t __gen_e_acsl__9;
double __gen_e_acsl_cast_3;
+ __e_acsl_mpq_t __gen_e_acsl__9;
__e_acsl_mpq_t __gen_e_acsl__10;
int __gen_e_acsl_ne_3;
__gmpq_init(__gen_e_acsl__8);
__gmpq_set_str(__gen_e_acsl__8,"01/10",10);
__gen_e_acsl_cast_2 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl_cast_3 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
__gmpq_init(__gen_e_acsl__9);
/*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_2); */
/*@ assert
Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl_cast_2);
*/
__gmpq_set_d(__gen_e_acsl__9,(double)((float)__gen_e_acsl_cast_2));
- __gen_e_acsl_cast_3 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
__gmpq_init(__gen_e_acsl__10);
/*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_3); */
__gmpq_set_d(__gen_e_acsl__10,__gen_e_acsl_cast_3);
@@ -122,32 +124,32 @@ int main(void)
double __gen_e_acsl_cast_4;
__e_acsl_mpq_t __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
__e_acsl_mpq_t __gen_e_acsl_add_2;
+ __e_acsl_mpq_t __gen_e_acsl__14;
int __gen_e_acsl_ne_4;
__gmpq_init(__gen_e_acsl__11);
__gmpq_set_str(__gen_e_acsl__11,"11/10",10);
__gen_e_acsl_cast_4 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
__gmpq_init(__gen_e_acsl__12);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_4); */
- __gmpq_set_d(__gen_e_acsl__12,__gen_e_acsl_cast_4);
+ __gmpq_set_str(__gen_e_acsl__12,"1",10);
__gmpq_init(__gen_e_acsl__13);
- __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_set_str(__gen_e_acsl__13,"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__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__12),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__12),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
+ __gmpq_init(__gen_e_acsl__14);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_4); */
+ __gmpq_set_d(__gen_e_acsl__14,__gen_e_acsl_cast_4);
+ __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__14),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",19);
__gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__12);
__gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
__gmpq_clear(__gen_e_acsl_add_2);
+ __gmpq_clear(__gen_e_acsl__14);
}
/*@ assert 1 + 0.1 ≡ 2 - 0.9; */
{
@@ -190,65 +192,86 @@ int main(void)
float sum = x + y;
/*@ assert sum ≢ x * y; */
{
- __e_acsl_mpq_t __gen_e_acsl_sum;
- __e_acsl_mpq_t __gen_e_acsl_x;
__e_acsl_mpq_t __gen_e_acsl_y;
+ __e_acsl_mpq_t __gen_e_acsl__19;
__e_acsl_mpq_t __gen_e_acsl_mul;
+ __e_acsl_mpq_t __gen_e_acsl__20;
int __gen_e_acsl_ne_5;
- __gmpq_init(__gen_e_acsl_sum);
- __gmpq_set_d(__gen_e_acsl_sum,(double)sum);
- __gmpq_init(__gen_e_acsl_x);
- __gmpq_set_d(__gen_e_acsl_x,(double)x);
__gmpq_init(__gen_e_acsl_y);
__gmpq_set_d(__gen_e_acsl_y,(double)y);
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_d(__gen_e_acsl__19,(double)x);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_sum),
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_d(__gen_e_acsl__20,(double)sum);
+ __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",24);
- __gmpq_clear(__gen_e_acsl_sum);
- __gmpq_clear(__gen_e_acsl_x);
__gmpq_clear(__gen_e_acsl_y);
+ __gmpq_clear(__gen_e_acsl__19);
__gmpq_clear(__gen_e_acsl_mul);
+ __gmpq_clear(__gen_e_acsl__20);
}
/*@ assert \let n = 1; 4 ≡ n + 3.0; */
{
int __gen_e_acsl_n;
- __e_acsl_mpq_t __gen_e_acsl__19;
- __e_acsl_mpq_t __gen_e_acsl_n_2;
- __e_acsl_mpq_t __gen_e_acsl__20;
+ __e_acsl_mpq_t __gen_e_acsl__21;
+ __e_acsl_mpq_t __gen_e_acsl__22;
+ __e_acsl_mpq_t __gen_e_acsl__23;
__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__19);
- __gmpq_set_str(__gen_e_acsl__19,"4",10);
- __gmpq_init(__gen_e_acsl_n_2);
- __gmpq_set_si(__gen_e_acsl_n_2,(long)__gen_e_acsl_n);
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_str(__gen_e_acsl__20,"30/10",10);
+ __gmpq_init(__gen_e_acsl__21);
+ __gmpq_set_str(__gen_e_acsl__21,"4",10);
+ __gmpq_init(__gen_e_acsl__22);
+ __gmpq_set_str(__gen_e_acsl__22,"30/10",10);
+ __gmpq_init(__gen_e_acsl__23);
+ __gmpq_set_si(__gen_e_acsl__23,(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_n_2),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__20));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__19),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__22));
+ __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
(__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);
- __gmpq_clear(__gen_e_acsl__19);
- __gmpq_clear(__gen_e_acsl_n_2);
- __gmpq_clear(__gen_e_acsl__20);
+ __gmpq_clear(__gen_e_acsl__21);
+ __gmpq_clear(__gen_e_acsl__22);
+ __gmpq_clear(__gen_e_acsl__23);
__gmpq_clear(__gen_e_acsl_add_4);
}
double d = 0.1;
__gen_e_acsl_avg(4.3,11.7);
- long double ld = 0.1l;
- /*@ assert d + 1 ≢ ld + 1; */ ;
- /*@ assert 1.1d ≢ 1 + 0.1; */ ;
- /*@ assert 3 ≢ 1e5; */ ;
- /*@ assert \let n = 99999999999999999999999999; 4 ≢ n + 3.7; */ ;
+ /*@ assert 1.1d ≢ 1 + 0.1; */
+ {
+ __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_5;
+ int __gen_e_acsl_ne_6;
+ __gmpq_init(__gen_e_acsl__24);
+ __gmpq_set_str(__gen_e_acsl__24,"1.1d",10);
+ __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));
+ __gen_e_acsl_ne_6 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
+ __e_acsl_assert(__gen_e_acsl_ne_6 != 0,(char *)"Assertion",
+ (char *)"main",(char *)"1.1d != 1 + 0.1",31);
+ __gmpq_clear(__gen_e_acsl__24);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
+ __gmpq_clear(__gen_e_acsl_add_5);
+ }
__retres = 0;
return __retres;
}
@@ -259,18 +282,10 @@ int main(void)
*/
double __gen_e_acsl_avg(double a, double b)
{
- __e_acsl_mpq_t __gen_e_acsl_at_2;
+ double __gen_e_acsl_at_2;
__e_acsl_mpq_t __gen_e_acsl_at;
double __retres;
- {
- __e_acsl_mpq_t __gen_e_acsl_b;
- __gmpq_init(__gen_e_acsl_b);
- __gmpq_set_d(__gen_e_acsl_b,b);
- __gmpq_init(__gen_e_acsl_at_2);
- __gmpq_set(__gen_e_acsl_at_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
- __gmpq_clear(__gen_e_acsl_b);
- }
+ __gen_e_acsl_at_2 = b;
{
__e_acsl_mpq_t __gen_e_acsl_a;
__gmpq_init(__gen_e_acsl_a);
@@ -283,25 +298,28 @@ double __gen_e_acsl_avg(double a, double b)
{
int __gen_e_acsl_delta;
__e_acsl_mpq_t __gen_e_acsl_avg_real;
- __e_acsl_mpq_t __gen_e_acsl_add;
__e_acsl_mpq_t __gen_e_acsl_;
+ __e_acsl_mpq_t __gen_e_acsl_add;
+ __e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl_div;
__e_acsl_mpq_t __gen_e_acsl_delta_2;
__e_acsl_mpq_t __gen_e_acsl_sub;
- __e_acsl_mpq_t __gen_e_acsl_result;
+ __e_acsl_mpq_t __gen_e_acsl__3;
int __gen_e_acsl_lt;
int __gen_e_acsl_and;
__gen_e_acsl_delta = 1;
+ __gmpq_init(__gen_e_acsl_);
+ __gmpq_set_d(__gen_e_acsl_,__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2));
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_str(__gen_e_acsl_,"2",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
+ __gmpq_init(__gen_e_acsl__2);
+ __gmpq_set_str(__gen_e_acsl__2,"2",10);
__gmpq_init(__gen_e_acsl_div);
__gmpq_div(__gen_e_acsl_div,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
__gmpq_init(__gen_e_acsl_avg_real);
__gmpq_set(__gen_e_acsl_avg_real,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
@@ -311,43 +329,43 @@ double __gen_e_acsl_avg(double a, double b)
__gmpq_sub(__gen_e_acsl_sub,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_delta_2));
- __gmpq_init(__gen_e_acsl_result);
- __gmpq_set_d(__gen_e_acsl_result,__retres);
+ __gmpq_init(__gen_e_acsl__3);
+ __gmpq_set_d(__gen_e_acsl__3,__retres);
__gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_result));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
if (__gen_e_acsl_lt < 0) {
- __e_acsl_mpq_t __gen_e_acsl_result_2;
__e_acsl_mpq_t __gen_e_acsl_delta_3;
__e_acsl_mpq_t __gen_e_acsl_add_2;
+ __e_acsl_mpq_t __gen_e_acsl__4;
int __gen_e_acsl_lt_2;
- __gmpq_init(__gen_e_acsl_result_2);
- __gmpq_set_d(__gen_e_acsl_result_2,__retres);
__gmpq_init(__gen_e_acsl_delta_3);
__gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_delta_3));
- __gen_e_acsl_lt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_result_2),
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_d(__gen_e_acsl__4,__retres);
+ __gen_e_acsl_lt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__gen_e_acsl_and = __gen_e_acsl_lt_2 < 0;
- __gmpq_clear(__gen_e_acsl_result_2);
__gmpq_clear(__gen_e_acsl_delta_3);
__gmpq_clear(__gen_e_acsl_add_2);
+ __gmpq_clear(__gen_e_acsl__4);
}
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);
__gmpq_clear(__gen_e_acsl_avg_real);
- __gmpq_clear(__gen_e_acsl_add);
__gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl_add);
+ __gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl_div);
__gmpq_clear(__gen_e_acsl_delta_2);
__gmpq_clear(__gen_e_acsl_sub);
- __gmpq_clear(__gen_e_acsl_result);
+ __gmpq_clear(__gen_e_acsl__3);
__gmpq_clear(__gen_e_acsl_at);
- __gmpq_clear(__gen_e_acsl_at_2);
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 6bba81c1a8918212a07a50ff815639fe1a6cfa5b..7627bd75e465e994363437329d9248bf68129f77 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
+++ b/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
@@ -1,6 +1,8 @@
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
+extern int __e_acsl_sound_verdict;
+
/*@ ensures \let delta = 1;
\let avg_real = (\old(a) + \old(b)) / 2;
avg_real - delta < \result < avg_real + delta;
@@ -91,20 +93,20 @@ int main(void)
{
__e_acsl_mpq_t __gen_e_acsl__8;
double __gen_e_acsl_cast_2;
- __e_acsl_mpq_t __gen_e_acsl__9;
double __gen_e_acsl_cast_3;
+ __e_acsl_mpq_t __gen_e_acsl__9;
__e_acsl_mpq_t __gen_e_acsl__10;
int __gen_e_acsl_ne_3;
__gmpq_init(__gen_e_acsl__8);
__gmpq_set_str(__gen_e_acsl__8,"01/10",10);
__gen_e_acsl_cast_2 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
+ __gen_e_acsl_cast_3 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
__gmpq_init(__gen_e_acsl__9);
/*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_2); */
/*@ assert
Eva: is_nan_or_infinite: \is_finite((float)__gen_e_acsl_cast_2);
*/
__gmpq_set_d(__gen_e_acsl__9,(double)((float)__gen_e_acsl_cast_2));
- __gen_e_acsl_cast_3 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__8));
__gmpq_init(__gen_e_acsl__10);
/*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_3); */
__gmpq_set_d(__gen_e_acsl__10,__gen_e_acsl_cast_3);
@@ -122,32 +124,32 @@ int main(void)
double __gen_e_acsl_cast_4;
__e_acsl_mpq_t __gen_e_acsl__12;
__e_acsl_mpq_t __gen_e_acsl__13;
- __e_acsl_mpq_t __gen_e_acsl__14;
__e_acsl_mpq_t __gen_e_acsl_add_2;
+ __e_acsl_mpq_t __gen_e_acsl__14;
int __gen_e_acsl_ne_4;
__gmpq_init(__gen_e_acsl__11);
__gmpq_set_str(__gen_e_acsl__11,"11/10",10);
__gen_e_acsl_cast_4 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
__gmpq_init(__gen_e_acsl__12);
- /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_4); */
- __gmpq_set_d(__gen_e_acsl__12,__gen_e_acsl_cast_4);
+ __gmpq_set_str(__gen_e_acsl__12,"1",10);
__gmpq_init(__gen_e_acsl__13);
- __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_set_str(__gen_e_acsl__13,"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__13),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
- __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__12),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__12),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
+ __gmpq_init(__gen_e_acsl__14);
+ /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast_4); */
+ __gmpq_set_d(__gen_e_acsl__14,__gen_e_acsl_cast_4);
+ __gen_e_acsl_ne_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__14),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__e_acsl_assert(__gen_e_acsl_ne_4 != 0,(char *)"Assertion",
(char *)"main",(char *)"(double)1.1 != 1 + 0.1",19);
__gmpq_clear(__gen_e_acsl__11);
__gmpq_clear(__gen_e_acsl__12);
__gmpq_clear(__gen_e_acsl__13);
- __gmpq_clear(__gen_e_acsl__14);
__gmpq_clear(__gen_e_acsl_add_2);
+ __gmpq_clear(__gen_e_acsl__14);
}
/*@ assert 1 + 0.1 ≡ 2 - 0.9; */
{
@@ -190,65 +192,86 @@ int main(void)
float sum = x + y;
/*@ assert sum ≢ x * y; */
{
- __e_acsl_mpq_t __gen_e_acsl_sum;
- __e_acsl_mpq_t __gen_e_acsl_x;
__e_acsl_mpq_t __gen_e_acsl_y;
+ __e_acsl_mpq_t __gen_e_acsl__19;
__e_acsl_mpq_t __gen_e_acsl_mul;
+ __e_acsl_mpq_t __gen_e_acsl__20;
int __gen_e_acsl_ne_5;
- __gmpq_init(__gen_e_acsl_sum);
- __gmpq_set_d(__gen_e_acsl_sum,(double)sum);
- __gmpq_init(__gen_e_acsl_x);
- __gmpq_set_d(__gen_e_acsl_x,(double)x);
__gmpq_init(__gen_e_acsl_y);
__gmpq_set_d(__gen_e_acsl_y,(double)y);
+ __gmpq_init(__gen_e_acsl__19);
+ __gmpq_set_d(__gen_e_acsl__19,(double)x);
__gmpq_init(__gen_e_acsl_mul);
__gmpq_mul(__gen_e_acsl_mul,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_x),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__19),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_y));
- __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_sum),
+ __gmpq_init(__gen_e_acsl__20);
+ __gmpq_set_d(__gen_e_acsl__20,(double)sum);
+ __gen_e_acsl_ne_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__20),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_mul));
__e_acsl_assert(__gen_e_acsl_ne_5 != 0,(char *)"Assertion",
(char *)"main",(char *)"sum != x * y",24);
- __gmpq_clear(__gen_e_acsl_sum);
- __gmpq_clear(__gen_e_acsl_x);
__gmpq_clear(__gen_e_acsl_y);
+ __gmpq_clear(__gen_e_acsl__19);
__gmpq_clear(__gen_e_acsl_mul);
+ __gmpq_clear(__gen_e_acsl__20);
}
/*@ assert \let n = 1; 4 ≡ n + 3.0; */
{
int __gen_e_acsl_n;
- __e_acsl_mpq_t __gen_e_acsl__19;
- __e_acsl_mpq_t __gen_e_acsl_n_2;
- __e_acsl_mpq_t __gen_e_acsl__20;
+ __e_acsl_mpq_t __gen_e_acsl__21;
+ __e_acsl_mpq_t __gen_e_acsl__22;
+ __e_acsl_mpq_t __gen_e_acsl__23;
__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__19);
- __gmpq_set_str(__gen_e_acsl__19,"4",10);
- __gmpq_init(__gen_e_acsl_n_2);
- __gmpq_set_si(__gen_e_acsl_n_2,(long)__gen_e_acsl_n);
- __gmpq_init(__gen_e_acsl__20);
- __gmpq_set_str(__gen_e_acsl__20,"30/10",10);
+ __gmpq_init(__gen_e_acsl__21);
+ __gmpq_set_str(__gen_e_acsl__21,"4",10);
+ __gmpq_init(__gen_e_acsl__22);
+ __gmpq_set_str(__gen_e_acsl__22,"30/10",10);
+ __gmpq_init(__gen_e_acsl__23);
+ __gmpq_set_si(__gen_e_acsl__23,(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_n_2),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__20));
- __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__19),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__23),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__22));
+ __gen_e_acsl_eq_4 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__21),
(__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);
- __gmpq_clear(__gen_e_acsl__19);
- __gmpq_clear(__gen_e_acsl_n_2);
- __gmpq_clear(__gen_e_acsl__20);
+ __gmpq_clear(__gen_e_acsl__21);
+ __gmpq_clear(__gen_e_acsl__22);
+ __gmpq_clear(__gen_e_acsl__23);
__gmpq_clear(__gen_e_acsl_add_4);
}
double d = 0.1;
__gen_e_acsl_avg(4.3,11.7);
- long double ld = 0.1l;
- /*@ assert d + 1 ≢ ld + 1; */ ;
- /*@ assert 1.1d ≢ 1 + 0.1; */ ;
- /*@ assert 3 ≢ 1e5; */ ;
- /*@ assert \let n = 99999999999999999999999999; 4 ≢ n + 3.7; */ ;
+ /*@ assert 1.1d ≢ 1 + 0.1; */
+ {
+ __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_5;
+ int __gen_e_acsl_ne_6;
+ __gmpq_init(__gen_e_acsl__24);
+ __gmpq_set_str(__gen_e_acsl__24,"1.1d",10);
+ __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));
+ __gen_e_acsl_ne_6 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__24),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_add_5));
+ __e_acsl_assert(__gen_e_acsl_ne_6 != 0,(char *)"Assertion",
+ (char *)"main",(char *)"1.1d != 1 + 0.1",31);
+ __gmpq_clear(__gen_e_acsl__24);
+ __gmpq_clear(__gen_e_acsl__25);
+ __gmpq_clear(__gen_e_acsl__26);
+ __gmpq_clear(__gen_e_acsl_add_5);
+ }
__retres = 0;
return __retres;
}
@@ -259,18 +282,10 @@ int main(void)
*/
double __gen_e_acsl_avg(double a, double b)
{
- __e_acsl_mpq_t __gen_e_acsl_at_2;
+ double __gen_e_acsl_at_2;
__e_acsl_mpq_t __gen_e_acsl_at;
double __retres;
- {
- __e_acsl_mpq_t __gen_e_acsl_b;
- __gmpq_init(__gen_e_acsl_b);
- __gmpq_set_d(__gen_e_acsl_b,b);
- __gmpq_init(__gen_e_acsl_at_2);
- __gmpq_set(__gen_e_acsl_at_2,
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
- __gmpq_clear(__gen_e_acsl_b);
- }
+ __gen_e_acsl_at_2 = b;
{
__e_acsl_mpq_t __gen_e_acsl_a;
__gmpq_init(__gen_e_acsl_a);
@@ -283,25 +298,28 @@ double __gen_e_acsl_avg(double a, double b)
{
int __gen_e_acsl_delta;
__e_acsl_mpq_t __gen_e_acsl_avg_real;
- __e_acsl_mpq_t __gen_e_acsl_add;
__e_acsl_mpq_t __gen_e_acsl_;
+ __e_acsl_mpq_t __gen_e_acsl_add;
+ __e_acsl_mpq_t __gen_e_acsl__2;
__e_acsl_mpq_t __gen_e_acsl_div;
__e_acsl_mpq_t __gen_e_acsl_delta_2;
__e_acsl_mpq_t __gen_e_acsl_sub;
- __e_acsl_mpq_t __gen_e_acsl_result;
+ __e_acsl_mpq_t __gen_e_acsl__3;
int __gen_e_acsl_lt;
int __gen_e_acsl_and;
__gen_e_acsl_delta = 1;
+ __gmpq_init(__gen_e_acsl_);
+ __gmpq_set_d(__gen_e_acsl_,__gen_e_acsl_at_2);
__gmpq_init(__gen_e_acsl_add);
__gmpq_add(__gen_e_acsl_add,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_at),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_at_2));
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_str(__gen_e_acsl_,"2",10);
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
+ __gmpq_init(__gen_e_acsl__2);
+ __gmpq_set_str(__gen_e_acsl__2,"2",10);
__gmpq_init(__gen_e_acsl_div);
__gmpq_div(__gen_e_acsl_div,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
__gmpq_init(__gen_e_acsl_avg_real);
__gmpq_set(__gen_e_acsl_avg_real,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
@@ -311,43 +329,43 @@ double __gen_e_acsl_avg(double a, double b)
__gmpq_sub(__gen_e_acsl_sub,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_delta_2));
- __gmpq_init(__gen_e_acsl_result);
- __gmpq_set_d(__gen_e_acsl_result,__retres);
+ __gmpq_init(__gen_e_acsl__3);
+ __gmpq_set_d(__gen_e_acsl__3,__retres);
__gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_sub),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl_result));
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
if (__gen_e_acsl_lt < 0) {
- __e_acsl_mpq_t __gen_e_acsl_result_2;
__e_acsl_mpq_t __gen_e_acsl_delta_3;
__e_acsl_mpq_t __gen_e_acsl_add_2;
+ __e_acsl_mpq_t __gen_e_acsl__4;
int __gen_e_acsl_lt_2;
- __gmpq_init(__gen_e_acsl_result_2);
- __gmpq_set_d(__gen_e_acsl_result_2,__retres);
__gmpq_init(__gen_e_acsl_delta_3);
__gmpq_set_si(__gen_e_acsl_delta_3,(long)__gen_e_acsl_delta);
__gmpq_init(__gen_e_acsl_add_2);
__gmpq_add(__gen_e_acsl_add_2,
(__e_acsl_mpq_struct const *)(__gen_e_acsl_avg_real),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_delta_3));
- __gen_e_acsl_lt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_result_2),
+ __gmpq_init(__gen_e_acsl__4);
+ __gmpq_set_d(__gen_e_acsl__4,__retres);
+ __gen_e_acsl_lt_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__4),
(__e_acsl_mpq_struct const *)(__gen_e_acsl_add_2));
__gen_e_acsl_and = __gen_e_acsl_lt_2 < 0;
- __gmpq_clear(__gen_e_acsl_result_2);
__gmpq_clear(__gen_e_acsl_delta_3);
__gmpq_clear(__gen_e_acsl_add_2);
+ __gmpq_clear(__gen_e_acsl__4);
}
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);
__gmpq_clear(__gen_e_acsl_avg_real);
- __gmpq_clear(__gen_e_acsl_add);
__gmpq_clear(__gen_e_acsl_);
+ __gmpq_clear(__gen_e_acsl_add);
+ __gmpq_clear(__gen_e_acsl__2);
__gmpq_clear(__gen_e_acsl_div);
__gmpq_clear(__gen_e_acsl_delta_2);
__gmpq_clear(__gen_e_acsl_sub);
- __gmpq_clear(__gen_e_acsl_result);
+ __gmpq_clear(__gen_e_acsl__3);
__gmpq_clear(__gen_e_acsl_at);
- __gmpq_clear(__gen_e_acsl_at_2);
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 a78fea8aefe39c321fa534ca71723b4a388a926e..a1a5dd8416dc57984e6502155398de1c462b9a77 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
@@ -3,20 +3,6 @@
(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:33: Warning:
- E-ACSL construct `creating gmp from long double' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/reals.c:34: Warning:
- E-ACSL construct `number not written in decimal expansion'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/reals.c:35: Warning:
- E-ACSL construct `number not written in decimal expansion'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/reals.c:37: Warning:
- E-ACSL construct `reals: creating Q from Z' is not yet supported.
- Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -27,6 +13,7 @@
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__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 __gmpq_init
[eva] using specification for function __gmpq_set_str
@@ -78,7 +65,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:33: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:34: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:36: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:31: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:31: 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 a78fea8aefe39c321fa534ca71723b4a388a926e..a1a5dd8416dc57984e6502155398de1c462b9a77 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
@@ -3,20 +3,6 @@
(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:33: Warning:
- E-ACSL construct `creating gmp from long double' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/reals.c:34: Warning:
- E-ACSL construct `number not written in decimal expansion'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/reals.c:35: Warning:
- E-ACSL construct `number not written in decimal expansion'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/gmp/reals.c:37: Warning:
- E-ACSL construct `reals: creating Q from Z' is not yet supported.
- Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -27,6 +13,7 @@
__e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
__e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
__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 __gmpq_init
[eva] using specification for function __gmpq_set_str
@@ -78,7 +65,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:33: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:34: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:36: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:31: Warning: assertion got status unknown.
+[eva:alarm] tests/gmp/reals.c:31: 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 928cfdd7db546f674085e694dd60779dfcd125b7..d199b47504555a479b6268e2be5c6d64556f76ee 100644
--- a/src/plugins/e-acsl/tests/gmp/reals.c
+++ b/src/plugins/e-acsl/tests/gmp/reals.c
@@ -28,11 +28,12 @@ int main(void) {
avg(4.3, 11.7);
+ /*@ assert 1.1d != 1 + 0.1; */ ;
+
// Not yet:
- long double ld = 0.1l;
- /*@ assert d + 1 != ld + 1; */ ; // long double
- /*@ assert 1.1d != 1 + 0.1; */ ; // number not written in decimal expansion form
- /*@ assert 3 != 1e5; */ ; // number not written in decimal expansion form
- /*@ assert \let n = 99999999999999999999999999;
- 4 != n + 3.7; */ ; // creating Q from Z
-}
\ No newline at end of file
+ // long double ld = 0.1l;
+ // /*@ assert d + 1 != ld + 1; */ ; // long double
+ // /*@ assert 3 != 1e5; */ ; // number not written in decimal expansion form
+ ///*@ assert \let n = 99999999999999999999999999;
+ // 4 != n + 3.7; */ ; // creating Q from Z
+}