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 cc5b0778cf10d9fcb9964f247f22b0cd626969f6..bb5a7cd1b3c49b8c32e0f0e920d1c1116b32fc3d 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,71 +1,73 @@
[e-acsl] beginning translation.
-[e-acsl] functions.c:70: Warning:
+[e-acsl] functions.c:73: Warning:
E-ACSL construct `function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions.c:48: Warning:
+[eva:alarm] functions.c:51: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:48: Warning:
+[eva:alarm] functions.c:51: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:50: Warning:
+[eva:alarm] functions.c:53: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:52: Warning:
+[eva:alarm] functions.c:55: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:52: Warning:
+[eva:alarm] functions.c:55: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:53: Warning:
+[eva:alarm] functions.c:56: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:53: Warning:
+[eva:alarm] functions.c:56: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:54: Warning:
+[eva:alarm] functions.c:57: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:55: Warning:
+[eva:alarm] functions.c:58: 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_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:63: Warning:
+[eva:alarm] functions.c:66: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:63: Warning:
+[eva:alarm] functions.c:66: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:65: Warning:
+[eva:alarm] functions.c:68: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:65: Warning:
+[eva:alarm] functions.c:68: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:70: Warning:
+[eva:alarm] functions.c:73: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:70: Warning:
+[eva:alarm] functions.c:73: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:70: Warning: assertion got status unknown.
-[eva:alarm] functions.c:71: Warning:
+[eva:alarm] functions.c:73: Warning: assertion got status unknown.
+[eva:alarm] functions.c:74: Warning:
function __e_acsl_assert_register_struct: 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_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:76: Warning:
+[eva:alarm] functions.c:79: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] functions.c:76: Warning:
+[eva:alarm] functions.c:79: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:76: Warning:
+[eva:alarm] functions.c:79: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] functions.c:81: Warning: assertion got status unknown.
+[eva:alarm] functions.c:83: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:78: Warning: assertion 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 7d6406619dfbbc8f4acb6b53e2f2e1e9db0eba91..8699808b755da65ff31130e928f3a703b1a85726 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -57,7 +57,7 @@ int __gen_e_acsl_g(int x);
/*@ logic mystruct t1(mystruct m) = m;
*/
-mystruct __gen_e_acsl_t1(mystruct m);
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m);
/*@ logic integer t2(mystruct m) = m.k + m.l;
*/
@@ -88,9 +88,13 @@ double __gen_e_acsl_f2(double x);
/*@ logic integer f_notyet{L}(integer x) = x;
*/
/*@ logic integer f_sum(integer x) = \sum(1, x, \lambda integer y; 1);
+ */
+int __gen_e_acsl_f_sum(int x);
+
+/*@ logic real over(real a, real b) = a / b;
*/
-int __gen_e_acsl_f_sum(int x);
+void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b);
int main(void)
{
@@ -112,7 +116,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 = 48;
+ __gen_e_acsl_assert_data.line = 51;
__e_acsl_assert(__gen_e_acsl_p1_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -129,7 +133,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 = 49;
+ __gen_e_acsl_assert_data_2.line = 52;
__e_acsl_assert(__gen_e_acsl_p2_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
@@ -150,7 +154,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 = 50;
+ __gen_e_acsl_assert_data_3.line = 53;
__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_);
@@ -170,7 +174,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 = 52;
+ __gen_e_acsl_assert_data_4.line = 55;
__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);
}
@@ -192,7 +196,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 = 53;
+ __gen_e_acsl_assert_data_5.line = 56;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
}
@@ -218,7 +222,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 = 54;
+ __gen_e_acsl_assert_data_6.line = 57;
__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);
@@ -249,7 +253,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 = 55;
+ __gen_e_acsl_assert_data_7.line = 58;
__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);
@@ -275,7 +279,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 = 60;
+ __gen_e_acsl_assert_data_8.line = 63;
__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);
}
@@ -295,7 +299,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 = 63;
+ __gen_e_acsl_assert_data_9.line = 66;
__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);
@@ -316,7 +320,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 = 65;
+ __gen_e_acsl_assert_data_10.line = 68;
__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);
@@ -329,7 +333,7 @@ int main(void)
mystruct __gen_e_acsl_t1_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
- __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t1(& __gen_e_acsl_t1_2,m);
__gen_e_acsl_r = __gen_e_acsl_t1_2;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_11,"r.k",0,
__gen_e_acsl_r.k);
@@ -340,7 +344,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 = 70;
+ __gen_e_acsl_assert_data_11.line = 73;
__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);
}
@@ -350,7 +354,7 @@ int main(void)
long __gen_e_acsl_t2_2;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_12 =
{.values = (void *)0};
- __gen_e_acsl_t1_4 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t1(& __gen_e_acsl_t1_4,m);
__gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_4);
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"m");
__e_acsl_assert_register_struct(& __gen_e_acsl_assert_data_12,"t1(m)");
@@ -361,7 +365,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 = 71;
+ __gen_e_acsl_assert_data_12.line = 74;
__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);
}
@@ -381,7 +385,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 = 76;
+ __gen_e_acsl_assert_data_13.line = 79;
__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);
}
@@ -398,12 +402,48 @@ 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 = 78;
+ __gen_e_acsl_assert_data_14.line = 81;
__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);
}
/*@ assert f_sum(100) == 100; */ ;
+ {
+ __e_acsl_mpq_t __gen_e_acsl_over_2;
+ __e_acsl_mpq_t __gen_e_acsl__11;
+ __e_acsl_mpq_t __gen_e_acsl__12;
+ __e_acsl_mpq_t __gen_e_acsl_div_3;
+ int __gen_e_acsl_eq_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_15 =
+ {.values = (void *)0};
+ __gen_e_acsl_over(& __gen_e_acsl_over_2,1.,2.);
+ __gmpq_init(__gen_e_acsl__11);
+ __gmpq_set_d(__gen_e_acsl__11,1.);
+ __gmpq_init(__gen_e_acsl__12);
+ __gmpq_set_d(__gen_e_acsl__12,2.);
+ __gmpq_init(__gen_e_acsl_div_3);
+ __gmpq_div(__gen_e_acsl_div_3,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__11),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__12));
+ __gen_e_acsl_eq_2 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_div_3));
+ __e_acsl_assert_register_mpq(& __gen_e_acsl_assert_data_15,
+ "over(1., 2.)",
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_over_2));
+ __gen_e_acsl_assert_data_15.blocking = 1;
+ __gen_e_acsl_assert_data_15.kind = "Assertion";
+ __gen_e_acsl_assert_data_15.pred_txt = "over(1., 2.) == 1. / 2.";
+ __gen_e_acsl_assert_data_15.file = "functions.c";
+ __gen_e_acsl_assert_data_15.fct = "main";
+ __gen_e_acsl_assert_data_15.line = 83;
+ __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);
+ __gmpq_clear(__gen_e_acsl__11);
+ __gmpq_clear(__gen_e_acsl__12);
+ __gmpq_clear(__gen_e_acsl_div_3);
+ }
+ /*@ assert over(1., 2.) == 1. / 2.; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
@@ -561,11 +601,12 @@ int __gen_e_acsl_g(int x)
return __gen_e_acsl_g_hidden_2;
}
-/*@ assigns \result;
- assigns \result \from m; */
-mystruct __gen_e_acsl_t1(mystruct m)
+/*@ assigns __retres_arg;
+ assigns __retres_arg \from m; */
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m)
{
- return m;
+ *__retres_arg = m;
+ return;
}
/*@ assigns \result;
@@ -633,4 +674,27 @@ int __gen_e_acsl_f_sum(int x)
return __gen_e_acsl_accumulator;
}
+/*@ assigns (*__retres_arg)[0];
+ assigns (*__retres_arg)[0] \from a, b; */
+void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b)
+{
+ __e_acsl_mpq_t __gen_e_acsl_b;
+ __e_acsl_mpq_t __gen_e_acsl__10;
+ __e_acsl_mpq_t __gen_e_acsl_div_2;
+ __gmpq_init(__gen_e_acsl_b);
+ __gmpq_set_d(__gen_e_acsl_b,b);
+ __gmpq_init(__gen_e_acsl__10);
+ __gmpq_set_d(__gen_e_acsl__10,a);
+ __gmpq_init(__gen_e_acsl_div_2);
+ __gmpq_div(__gen_e_acsl_div_2,
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl__10),
+ (__e_acsl_mpq_struct const *)(__gen_e_acsl_b));
+ __gmpq_init(*__retres_arg);
+ __gmpq_set(*__retres_arg,(__e_acsl_mpq_struct const *)(__gen_e_acsl_div_2));
+ __gmpq_clear(__gen_e_acsl_b);
+ __gmpq_clear(__gen_e_acsl__10);
+ __gmpq_clear(__gen_e_acsl_div_2);
+ return;
+}
+
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
index 11e868ecff42b57483b231fea8c40d5782b95b31..8dacca6e91c64b25bd74aff9816d9713734b3a5f 100644
--- a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
@@ -58,7 +58,7 @@ int __gen_e_acsl_g(int x);
/*@ logic mystruct t1(mystruct m) = m;
*/
-mystruct __gen_e_acsl_t1(mystruct m);
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m);
/*@ logic integer t2(mystruct m) = m.k + m.l;
*/
@@ -378,7 +378,7 @@ int main(void)
int __gen_e_acsl_eq_6;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_11 =
{.values = (void *)0};
- __gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
+ __gen_e_acsl_t1(& __gen_e_acsl_t1_2,m);
__gen_e_acsl_t2(& __gen_e_acsl_t2_2,__gen_e_acsl_t1_2);
__gmpz_init_set_si(__gen_e_acsl__16,17L);
__gen_e_acsl_eq_6 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_t2_2),
@@ -657,11 +657,12 @@ int __gen_e_acsl_g(int x)
return __gen_e_acsl_g_hidden_2;
}
-/*@ assigns \result;
- assigns \result \from m; */
-mystruct __gen_e_acsl_t1(mystruct m)
+/*@ assigns __retres_arg;
+ assigns __retres_arg \from m; */
+void __gen_e_acsl_t1(mystruct *__retres_arg, mystruct m)
{
- return m;
+ *__retres_arg = m;
+ return;
}
/*@ assigns (*__retres_arg)[0];