diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index c2f641d12e679ad153032a3f562fd5692e4cd464..e7cd2d6a7fea29e37d29d29638e5b22d3e3fefaa 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,8 @@
Plugin E-ACSL <next-release>
###############################################################################
+-* E-ACSL [2024-06-20] fix typing of logic functions over rationals
+
###############################################################################
Plugin E-ACSL 29.0 (Copper)
###############################################################################
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index c51ffd5bd0439aee40b0ef4e236b8008ea5a11bf..d226daab37b0c959d893164c6e7c2f5d43a27349 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -46,6 +46,9 @@ int glob = 5;
// Test functions returning a rational
/*@ logic real over(real a, real b) = a/b; */
+// Test functions using a rational
+/*@ logic integer signum(â„ x) = x > 0. ? 1 : x < 0. ? -1 : 0; */
+
//Test function using a global variable (they elaborate to functions
//with labels)
int z = 8;
@@ -91,4 +94,8 @@ int main(void) {
/*@ assert f_here(27) == 27; */;
/*@ assert f3(5) == 13; */;
+
+ /*@ assert signum(3.0) > 0; */
+ /*@ assert signum(0.0-3.0) < 0; */
+ /*@ assert signum(0.0) ≡ 0; */
}
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
index 54197511b15e324dbbfc3335111e1dff382fa499..b45b4d727ceb341debedf941fc93c446accf8d72 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,73 +1,75 @@
[e-acsl] beginning translation.
-[e-acsl] functions.c:78: Warning:
+[e-acsl] functions.c:81: Warning:
E-ACSL construct `function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions.c:56: Warning:
+[eva:alarm] functions.c:59: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:56: Warning:
+[eva:alarm] functions.c:59: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:58: Warning:
+[eva:alarm] functions.c:61: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:60: Warning:
+[eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:60: Warning:
+[eva:alarm] functions.c:63: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:61: Warning:
+[eva:alarm] functions.c:64: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:61: Warning:
+[eva:alarm] functions.c:64: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:62: Warning:
+[eva:alarm] functions.c:65: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:63: Warning:
+[eva:alarm] functions.c:66: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:68: Warning:
+[eva:alarm] functions.c:71: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:68: Warning:
+[eva:alarm] functions.c:71: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:71: Warning:
+[eva:alarm] functions.c:74: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:71: Warning:
+[eva:alarm] functions.c:74: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:73: Warning:
+[eva:alarm] functions.c:76: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:73: Warning:
+[eva:alarm] functions.c:76: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:78: Warning:
+[eva:alarm] functions.c:81: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:78: Warning:
+[eva:alarm] functions.c:81: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:78: Warning: assertion got status unknown.
-[eva:alarm] functions.c:79: Warning:
+[eva:alarm] functions.c:81: Warning: assertion got status unknown.
+[eva:alarm] functions.c:82: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:79: Warning:
+[eva:alarm] functions.c:82: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
[eva:alarm] functions.c:28: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:84: Warning:
+[eva:alarm] functions.c:87: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__8);
-[eva:alarm] functions.c:84: Warning:
+[eva:alarm] functions.c:87: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:84: Warning:
+[eva:alarm] functions.c:87: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] functions.c:89: Warning: assertion got status unknown.
+[eva:alarm] functions.c:91: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:86: Warning: assertion got status unknown.
-[eva:alarm] functions.c:88: Warning:
+[eva:alarm] functions.c:99: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
index c93894f5c0b3395cb8211104eb52ddcaed0875db..8f65ae1ddbe86eddcf092a038e9e5ab452c9ec82 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -100,6 +100,15 @@ int __gen_e_acsl_f_sum(int x);
*/
void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b);
+/*@ logic integer signum(real x) = x > 0.? 1: (x < 0.? -1: 0);
+
+*/
+int __gen_e_acsl_signum_5(double x);
+
+int __gen_e_acsl_signum(double x);
+
+int __gen_e_acsl_signum_3(__e_acsl_mpq_t x);
+
int z = 8;
/*@ logic integer f3{L}(integer y) = \at(z + y,L);
@@ -126,7 +135,7 @@ int main(void)
__gen_e_acsl_assert_data.pred_txt = "p1(x, y)";
__gen_e_acsl_assert_data.file = "functions.c";
__gen_e_acsl_assert_data.fct = "main";
- __gen_e_acsl_assert_data.line = 56;
+ __gen_e_acsl_assert_data.line = 59;
__e_acsl_assert(__gen_e_acsl_p1_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -143,7 +152,7 @@ int main(void)
__gen_e_acsl_assert_data_2.pred_txt = "p2(3, 4)";
__gen_e_acsl_assert_data_2.file = "functions.c";
__gen_e_acsl_assert_data_2.fct = "main";
- __gen_e_acsl_assert_data_2.line = 57;
+ __gen_e_acsl_assert_data_2.line = 60;
__e_acsl_assert(__gen_e_acsl_p2_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
@@ -164,7 +173,7 @@ int main(void)
__gen_e_acsl_assert_data_3.pred_txt = "p2(5, 99999999999999999999999999999)";
__gen_e_acsl_assert_data_3.file = "functions.c";
__gen_e_acsl_assert_data_3.fct = "main";
- __gen_e_acsl_assert_data_3.line = 58;
+ __gen_e_acsl_assert_data_3.line = 61;
__e_acsl_assert(__gen_e_acsl_p2_4,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
__gmpz_clear(__gen_e_acsl_);
@@ -184,7 +193,7 @@ int main(void)
__gen_e_acsl_assert_data_4.pred_txt = "f1(x, y) == 3";
__gen_e_acsl_assert_data_4.file = "functions.c";
__gen_e_acsl_assert_data_4.fct = "main";
- __gen_e_acsl_assert_data_4.line = 60;
+ __gen_e_acsl_assert_data_4.line = 63;
__e_acsl_assert(__gen_e_acsl_f1_2 == 3L,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
@@ -206,7 +215,7 @@ int main(void)
__gen_e_acsl_assert_data_5.pred_txt = "p2(x, f1(3, 4))";
__gen_e_acsl_assert_data_5.file = "functions.c";
__gen_e_acsl_assert_data_5.fct = "main";
- __gen_e_acsl_assert_data_5.line = 61;
+ __gen_e_acsl_assert_data_5.line = 64;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
}
@@ -232,7 +241,7 @@ int main(void)
__gen_e_acsl_assert_data_6.pred_txt = "f1(9, 99999999999999999999999999999) > 0";
__gen_e_acsl_assert_data_6.file = "functions.c";
__gen_e_acsl_assert_data_6.fct = "main";
- __gen_e_acsl_assert_data_6.line = 62;
+ __gen_e_acsl_assert_data_6.line = 65;
__e_acsl_assert(__gen_e_acsl_gt_2 > 0,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
__gmpz_clear(__gen_e_acsl__3);
@@ -263,7 +272,7 @@ int main(void)
__gen_e_acsl_assert_data_7.pred_txt = "f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998";
__gen_e_acsl_assert_data_7.file = "functions.c";
__gen_e_acsl_assert_data_7.fct = "main";
- __gen_e_acsl_assert_data_7.line = 63;
+ __gen_e_acsl_assert_data_7.line = 66;
__e_acsl_assert(__gen_e_acsl_eq == 0,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
__gmpz_clear(__gen_e_acsl__5);
@@ -289,7 +298,7 @@ int main(void)
__gen_e_acsl_assert_data_8.pred_txt = "g(x) == x";
__gen_e_acsl_assert_data_8.file = "functions.c";
__gen_e_acsl_assert_data_8.fct = "main";
- __gen_e_acsl_assert_data_8.line = 68;
+ __gen_e_acsl_assert_data_8.line = 71;
__e_acsl_assert(__gen_e_acsl_g_2 == x,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
}
@@ -309,7 +318,7 @@ int main(void)
__gen_e_acsl_assert_data_9.pred_txt = "h_char(c) == c";
__gen_e_acsl_assert_data_9.file = "functions.c";
__gen_e_acsl_assert_data_9.fct = "main";
- __gen_e_acsl_assert_data_9.line = 71;
+ __gen_e_acsl_assert_data_9.line = 74;
__e_acsl_assert((int)__gen_e_acsl_h_char_2 == (int)c,
& __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
@@ -330,7 +339,7 @@ int main(void)
__gen_e_acsl_assert_data_10.pred_txt = "h_short(s) == s";
__gen_e_acsl_assert_data_10.file = "functions.c";
__gen_e_acsl_assert_data_10.fct = "main";
- __gen_e_acsl_assert_data_10.line = 73;
+ __gen_e_acsl_assert_data_10.line = 76;
__e_acsl_assert((int)__gen_e_acsl_h_short_2 == (int)s,
& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
@@ -354,7 +363,7 @@ int main(void)
__gen_e_acsl_assert_data_11.pred_txt = "\\let r = t1(m); r.k == 8";
__gen_e_acsl_assert_data_11.file = "functions.c";
__gen_e_acsl_assert_data_11.fct = "main";
- __gen_e_acsl_assert_data_11.line = 78;
+ __gen_e_acsl_assert_data_11.line = 81;
__e_acsl_assert(__gen_e_acsl_r.k == 8,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
}
@@ -375,7 +384,7 @@ int main(void)
__gen_e_acsl_assert_data_12.pred_txt = "t2(t1(m)) == 17";
__gen_e_acsl_assert_data_12.file = "functions.c";
__gen_e_acsl_assert_data_12.fct = "main";
- __gen_e_acsl_assert_data_12.line = 79;
+ __gen_e_acsl_assert_data_12.line = 82;
__e_acsl_assert(__gen_e_acsl_t2_2 == 17L,& __gen_e_acsl_assert_data_12);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_12);
}
@@ -395,7 +404,7 @@ int main(void)
__gen_e_acsl_assert_data_13.pred_txt = "f2(d) > 0";
__gen_e_acsl_assert_data_13.file = "functions.c";
__gen_e_acsl_assert_data_13.fct = "main";
- __gen_e_acsl_assert_data_13.line = 84;
+ __gen_e_acsl_assert_data_13.line = 87;
__e_acsl_assert(__gen_e_acsl_f2_2 > 0.,& __gen_e_acsl_assert_data_13);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_13);
}
@@ -412,7 +421,7 @@ int main(void)
__gen_e_acsl_assert_data_14.pred_txt = "f_sum(100) == 100";
__gen_e_acsl_assert_data_14.file = "functions.c";
__gen_e_acsl_assert_data_14.fct = "main";
- __gen_e_acsl_assert_data_14.line = 86;
+ __gen_e_acsl_assert_data_14.line = 89;
__e_acsl_assert(__gen_e_acsl_f_sum_2 == 100,
& __gen_e_acsl_assert_data_14);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_14);
@@ -437,7 +446,7 @@ int main(void)
__gen_e_acsl_assert_data_15.pred_txt = "over(1., 2.) == 0.5";
__gen_e_acsl_assert_data_15.file = "functions.c";
__gen_e_acsl_assert_data_15.fct = "main";
- __gen_e_acsl_assert_data_15.line = 88;
+ __gen_e_acsl_assert_data_15.line = 91;
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,& __gen_e_acsl_assert_data_15);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
__gmpq_clear(__gen_e_acsl_over_2);
@@ -456,7 +465,7 @@ int main(void)
__gen_e_acsl_assert_data_16.pred_txt = "p_here(27)";
__gen_e_acsl_assert_data_16.file = "functions.c";
__gen_e_acsl_assert_data_16.fct = "main";
- __gen_e_acsl_assert_data_16.line = 90;
+ __gen_e_acsl_assert_data_16.line = 93;
__e_acsl_assert(__gen_e_acsl_p_here_2,& __gen_e_acsl_assert_data_16);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
}
@@ -473,7 +482,7 @@ int main(void)
__gen_e_acsl_assert_data_17.pred_txt = "f_here(27) == 27";
__gen_e_acsl_assert_data_17.file = "functions.c";
__gen_e_acsl_assert_data_17.fct = "main";
- __gen_e_acsl_assert_data_17.line = 91;
+ __gen_e_acsl_assert_data_17.line = 94;
__e_acsl_assert(__gen_e_acsl_f_here_2 == 27,
& __gen_e_acsl_assert_data_17);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_17);
@@ -491,11 +500,76 @@ int main(void)
__gen_e_acsl_assert_data_18.pred_txt = "f3(5) == 13";
__gen_e_acsl_assert_data_18.file = "functions.c";
__gen_e_acsl_assert_data_18.fct = "main";
- __gen_e_acsl_assert_data_18.line = 93;
+ __gen_e_acsl_assert_data_18.line = 96;
__e_acsl_assert(__gen_e_acsl_f3_2 == 13L,& __gen_e_acsl_assert_data_18);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_18);
}
/*@ assert f3(5) == 13; */ ;
+ {
+ int __gen_e_acsl_signum_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_19 =
+ {.values = (void *)0};
+ __gen_e_acsl_signum_2 = __gen_e_acsl_signum(3.);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_19,"signum(3.0)",
+ 0,__gen_e_acsl_signum_2);
+ __gen_e_acsl_assert_data_19.blocking = 1;
+ __gen_e_acsl_assert_data_19.kind = "Assertion";
+ __gen_e_acsl_assert_data_19.pred_txt = "signum(3.0) > 0";
+ __gen_e_acsl_assert_data_19.file = "functions.c";
+ __gen_e_acsl_assert_data_19.fct = "main";
+ __gen_e_acsl_assert_data_19.line = 98;
+ __e_acsl_assert(__gen_e_acsl_signum_2 > 0,& __gen_e_acsl_assert_data_19);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_19);
+ }
+ /*@ assert signum(3.0) > 0; */ ;
+ {
+ __e_acsl_mpq_t __gen_e_acsl__10;
+ __e_acsl_mpq_t __gen_e_acsl__11;
+ __e_acsl_mpq_t __gen_e_acsl_sub;
+ int __gen_e_acsl_signum_4;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_20 =
+ {.values = (void *)0};
+ __gmpq_init(__gen_e_acsl__10);
+ __gmpq_set_d(__gen_e_acsl__10,0.);
+ __gmpq_init(__gen_e_acsl__11);
+ __gmpq_set_d(__gen_e_acsl__11,3.);
+ __gmpq_init(__gen_e_acsl_sub);
+ __gmpq_sub(__gen_e_acsl_sub,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__11));
+ __gen_e_acsl_signum_4 = __gen_e_acsl_signum_3(__gen_e_acsl_sub);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_20,
+ "signum(0.0 - 3.0)",0,__gen_e_acsl_signum_4);
+ __gen_e_acsl_assert_data_20.blocking = 1;
+ __gen_e_acsl_assert_data_20.kind = "Assertion";
+ __gen_e_acsl_assert_data_20.pred_txt = "signum(0.0 - 3.0) < 0";
+ __gen_e_acsl_assert_data_20.file = "functions.c";
+ __gen_e_acsl_assert_data_20.fct = "main";
+ __gen_e_acsl_assert_data_20.line = 99;
+ __e_acsl_assert(__gen_e_acsl_signum_4 < 0,& __gen_e_acsl_assert_data_20);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_20);
+ __gmpq_clear(__gen_e_acsl__10);
+ __gmpq_clear(__gen_e_acsl__11);
+ __gmpq_clear(__gen_e_acsl_sub);
+ }
+ /*@ assert signum(0.0 - 3.0) < 0; */ ;
+ {
+ int __gen_e_acsl_signum_6;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_21 =
+ {.values = (void *)0};
+ __gen_e_acsl_signum_6 = __gen_e_acsl_signum_5(0.);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_21,"signum(0.0)",
+ 0,__gen_e_acsl_signum_6);
+ __gen_e_acsl_assert_data_21.blocking = 1;
+ __gen_e_acsl_assert_data_21.kind = "Assertion";
+ __gen_e_acsl_assert_data_21.pred_txt = "signum(0.0) == 0";
+ __gen_e_acsl_assert_data_21.file = "functions.c";
+ __gen_e_acsl_assert_data_21.fct = "main";
+ __gen_e_acsl_assert_data_21.line = 100;
+ __e_acsl_assert(__gen_e_acsl_signum_6 == 0,& __gen_e_acsl_assert_data_21);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data_21);
+ }
+ /*@ assert signum(0.0) == 0; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
@@ -764,6 +838,63 @@ void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b)
return;
}
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_signum_5(double x)
+{
+ int __gen_e_acsl_if_6;
+ if (x > 0.) __gen_e_acsl_if_6 = 1;
+ else {
+ int __gen_e_acsl_if_5;
+ if (x < 0.) __gen_e_acsl_if_5 = -1; else __gen_e_acsl_if_5 = 0;
+ __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
+ }
+ return __gen_e_acsl_if_6;
+}
+
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_signum(double x)
+{
+ int __gen_e_acsl_if_2;
+ if (x > 0.) __gen_e_acsl_if_2 = 1;
+ else {
+ int __gen_e_acsl_if;
+ if (x < 0.) __gen_e_acsl_if = -1; else __gen_e_acsl_if = 0;
+ __gen_e_acsl_if_2 = __gen_e_acsl_if;
+ }
+ return __gen_e_acsl_if_2;
+}
+
+/*@ assigns \result;
+ assigns \result \from *((__e_acsl_mpq_struct *)x); */
+int __gen_e_acsl_signum_3(__e_acsl_mpq_t x)
+{
+ __e_acsl_mpq_t __gen_e_acsl__12;
+ int __gen_e_acsl_gt_3;
+ int __gen_e_acsl_if_4;
+ __gmpq_init(__gen_e_acsl__12);
+ __gmpq_set_d(__gen_e_acsl__12,0.);
+ __gen_e_acsl_gt_3 = __gmpq_cmp((__e_acsl_mpq_struct const *)(x),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__12));
+ if (__gen_e_acsl_gt_3 > 0) __gen_e_acsl_if_4 = 1;
+ else {
+ __e_acsl_mpq_t __gen_e_acsl__13;
+ int __gen_e_acsl_lt;
+ int __gen_e_acsl_if_3;
+ __gmpq_init(__gen_e_acsl__13);
+ __gmpq_set_d(__gen_e_acsl__13,0.);
+ __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(x),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__13));
+ if (__gen_e_acsl_lt < 0) __gen_e_acsl_if_3 = -1;
+ else __gen_e_acsl_if_3 = 0;
+ __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
+ __gmpq_clear(__gen_e_acsl__13);
+ }
+ __gmpq_clear(__gen_e_acsl__12);
+ return __gen_e_acsl_if_4;
+}
+
/*@ assigns \result;
assigns \result \from y; */
long __gen_e_acsl_f3(int y)
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c
deleted file mode 100644
index 1fa5198a8166bf42ac9b36acd2eb66f794837cc9..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_sign_rational.c
+++ /dev/null
@@ -1,149 +0,0 @@
-/* Generated by Frama-C */
-#include "pthread.h"
-#include "sched.h"
-#include "signal.h"
-#include "stddef.h"
-#include "stdint.h"
-#include "stdio.h"
-#include "time.h"
-extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
-
-/*@ logic integer signum(real x) = x > 0.? 1: (x < 0.? -1: 0);
-
-*/
-int __gen_e_acsl_signum_5(double x);
-
-int __gen_e_acsl_signum(double x);
-
-int __gen_e_acsl_signum_3(__e_acsl_mpq_t x);
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,8UL);
- {
- int __gen_e_acsl_signum_2;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
- __gen_e_acsl_signum_2 = __gen_e_acsl_signum(3.);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"signum(3.0)",0,
- __gen_e_acsl_signum_2);
- __gen_e_acsl_assert_data.blocking = 1;
- __gen_e_acsl_assert_data.kind = "Assertion";
- __gen_e_acsl_assert_data.pred_txt = "signum(3.0) > 0";
- __gen_e_acsl_assert_data.file = "sign_rational.c";
- __gen_e_acsl_assert_data.fct = "main";
- __gen_e_acsl_assert_data.line = 11;
- __e_acsl_assert(__gen_e_acsl_signum_2 > 0,& __gen_e_acsl_assert_data);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
- }
- /*@ assert signum(3.0) > 0; */ ;
- {
- __e_acsl_mpq_t __gen_e_acsl_;
- __e_acsl_mpq_t __gen_e_acsl__2;
- __e_acsl_mpq_t __gen_e_acsl_sub;
- int __gen_e_acsl_signum_4;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_2 =
- {.values = (void *)0};
- __gmpq_init(__gen_e_acsl_);
- __gmpq_set_d(__gen_e_acsl_,0.);
- __gmpq_init(__gen_e_acsl__2);
- __gmpq_set_d(__gen_e_acsl__2,3.);
- __gmpq_init(__gen_e_acsl_sub);
- __gmpq_sub(__gen_e_acsl_sub,(__e_acsl_mpq_struct const *)(__gen_e_acsl_),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__2));
- __gen_e_acsl_signum_4 = __gen_e_acsl_signum_3(__gen_e_acsl_sub);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_2,
- "signum(0.0 - 3.0)",0,__gen_e_acsl_signum_4);
- __gen_e_acsl_assert_data_2.blocking = 1;
- __gen_e_acsl_assert_data_2.kind = "Assertion";
- __gen_e_acsl_assert_data_2.pred_txt = "signum(0.0 - 3.0) < 0";
- __gen_e_acsl_assert_data_2.file = "sign_rational.c";
- __gen_e_acsl_assert_data_2.fct = "main";
- __gen_e_acsl_assert_data_2.line = 12;
- __e_acsl_assert(__gen_e_acsl_signum_4 < 0,& __gen_e_acsl_assert_data_2);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
- __gmpq_clear(__gen_e_acsl_);
- __gmpq_clear(__gen_e_acsl__2);
- __gmpq_clear(__gen_e_acsl_sub);
- }
- /*@ assert signum(0.0 - 3.0) < 0; */ ;
- {
- int __gen_e_acsl_signum_6;
- __e_acsl_assert_data_t __gen_e_acsl_assert_data_3 =
- {.values = (void *)0};
- __gen_e_acsl_signum_6 = __gen_e_acsl_signum_5(0.);
- __e_acsl_assert_register_int(& __gen_e_acsl_assert_data_3,"signum(0.0)",
- 0,__gen_e_acsl_signum_6);
- __gen_e_acsl_assert_data_3.blocking = 1;
- __gen_e_acsl_assert_data_3.kind = "Assertion";
- __gen_e_acsl_assert_data_3.pred_txt = "signum(0.0) == 0";
- __gen_e_acsl_assert_data_3.file = "sign_rational.c";
- __gen_e_acsl_assert_data_3.fct = "main";
- __gen_e_acsl_assert_data_3.line = 13;
- __e_acsl_assert(__gen_e_acsl_signum_6 == 0,& __gen_e_acsl_assert_data_3);
- __e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
- }
- /*@ assert signum(0.0) == 0; */ ;
- __retres = 0;
- __e_acsl_memory_clean();
- return __retres;
-}
-
-/*@ assigns \result;
- assigns \result \from x; */
-int __gen_e_acsl_signum_5(double x)
-{
- int __gen_e_acsl_if_6;
- if (x > 0.) __gen_e_acsl_if_6 = 1;
- else {
- int __gen_e_acsl_if_5;
- if (x < 0.) __gen_e_acsl_if_5 = -1; else __gen_e_acsl_if_5 = 0;
- __gen_e_acsl_if_6 = __gen_e_acsl_if_5;
- }
- return __gen_e_acsl_if_6;
-}
-
-/*@ assigns \result;
- assigns \result \from x; */
-int __gen_e_acsl_signum(double x)
-{
- int __gen_e_acsl_if_2;
- if (x > 0.) __gen_e_acsl_if_2 = 1;
- else {
- int __gen_e_acsl_if;
- if (x < 0.) __gen_e_acsl_if = -1; else __gen_e_acsl_if = 0;
- __gen_e_acsl_if_2 = __gen_e_acsl_if;
- }
- return __gen_e_acsl_if_2;
-}
-
-/*@ assigns \result;
- assigns \result \from *((__e_acsl_mpq_struct *)x); */
-int __gen_e_acsl_signum_3(__e_acsl_mpq_t x)
-{
- __e_acsl_mpq_t __gen_e_acsl__3;
- int __gen_e_acsl_gt;
- int __gen_e_acsl_if_4;
- __gmpq_init(__gen_e_acsl__3);
- __gmpq_set_d(__gen_e_acsl__3,0.);
- __gen_e_acsl_gt = __gmpq_cmp((__e_acsl_mpq_struct const *)(x),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__3));
- if (__gen_e_acsl_gt > 0) __gen_e_acsl_if_4 = 1;
- else {
- __e_acsl_mpq_t __gen_e_acsl__4;
- int __gen_e_acsl_lt;
- int __gen_e_acsl_if_3;
- __gmpq_init(__gen_e_acsl__4);
- __gmpq_set_d(__gen_e_acsl__4,0.);
- __gen_e_acsl_lt = __gmpq_cmp((__e_acsl_mpq_struct const *)(x),
- (__e_acsl_mpq_struct const *)(__gen_e_acsl__4));
- if (__gen_e_acsl_lt < 0) __gen_e_acsl_if_3 = -1;
- else __gen_e_acsl_if_3 = 0;
- __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
- __gmpq_clear(__gen_e_acsl__4);
- }
- __gmpq_clear(__gen_e_acsl__3);
- return __gen_e_acsl_if_4;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle
deleted file mode 100644
index 1d33ef8c2a90e87a42879c53d962e739225f65a7..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/sign_rational.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] sign_rational.c:12: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/sign_rational.c b/src/plugins/e-acsl/tests/arith/sign_rational.c
deleted file mode 100644
index 34a823fb8320a1f2bd6d52ee9528b0b5013ac127..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/sign_rational.c
+++ /dev/null
@@ -1,15 +0,0 @@
-/* run.config
- COMMENT: a logic function defined over rationals
-*/
-
-/*@
- logic integer signum(â„ x) =
- x > 0. ? 1 : x < 0. ? -1 : 0;
-*/
-
-int main() {
- /*@ assert signum(3.0) > 0; */
- /*@ assert signum(0.0-3.0) < 0; */
- /*@ assert signum(0.0) ≡ 0; */
- return 0;
-}