diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index a3e010fc6f607b715aa78855b37b91d5012227ff..c51ffd5bd0439aee40b0ef4e236b8008ea5a11bf 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -46,6 +46,11 @@ int glob = 5;
// Test functions returning a rational
/*@ logic real over(real a, real b) = a/b; */
+//Test function using a global variable (they elaborate to functions
+//with labels)
+int z = 8;
+/*@ logic integer f3 (integer y) = z+y; */
+
int main(void) {
int x = 1, y = 2;
/*@ assert p1(x, y); */;
@@ -82,7 +87,8 @@ int main(void) {
/*@ assert over(1., 2.) == 0.5; */;
- // not yet supported
/*@ assert p_here(27); */;
/*@ assert f_here(27) == 27; */;
+
+ /*@ assert f3(5) == 13; */;
}
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 bb5a7cd1b3c49b8c32e0f0e920d1c1116b32fc3d..eeec870713379fa27db796bee36b86b1f32df353 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,73 @@
[e-acsl] beginning translation.
-[e-acsl] functions.c:73: Warning:
+[e-acsl] functions.c:78: Warning:
E-ACSL construct `function application' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] functions.c:51: 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:51: 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:58: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:55: Warning:
+[eva:alarm] functions.c:60: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:55: Warning:
+[eva:alarm] functions.c:60: Warning:
function __e_acsl_assert_register_long: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:56: Warning:
+[eva:alarm] functions.c:61: 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:61: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:57: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] functions.c:58: Warning:
+[eva:alarm] functions.c:62: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] functions.c:63: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] functions.c:68: 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:68: Warning:
function __e_acsl_assert_register_int: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:66: Warning:
+[eva:alarm] functions.c:71: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:66: Warning:
+[eva:alarm] functions.c:71: Warning:
function __e_acsl_assert_register_char: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:68: Warning:
+[eva:alarm] functions.c:73: Warning:
function __e_acsl_assert_register_short: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:68: Warning:
+[eva:alarm] functions.c:73: 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:78: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:73: Warning:
+[eva:alarm] functions.c:78: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:73: Warning: assertion got status unknown.
-[eva:alarm] functions.c:74: Warning:
+[eva:alarm] functions.c:78: Warning: assertion got status unknown.
+[eva:alarm] functions.c:79: Warning:
function __e_acsl_assert_register_struct: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:74: Warning:
+[eva:alarm] functions.c:79: 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:79: Warning:
+[eva:alarm] functions.c:84: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] functions.c:79: Warning:
+[eva:alarm] functions.c:84: Warning:
function __e_acsl_assert_register_double: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[eva:alarm] functions.c:79: Warning:
+[eva:alarm] functions.c:84: 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:
+[eva:alarm] functions.c:86: Warning: assertion got status unknown.
+[eva:alarm] functions.c:88: 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 c173eeb0c636c88c751bdf35ad302ec72cea7082..7aea7dc1b36ead4003a0ffb2ceb233a3e43b1f45 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,12 @@ int __gen_e_acsl_f_sum(int x);
*/
void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b);
+int z = 8;
+/*@ logic integer f3{L}(integer y) = \at(z + y,L);
+
+*/
+long __gen_e_acsl_f3(int y);
+
int main(void)
{
int __retres;
@@ -120,7 +126,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 = 51;
+ __gen_e_acsl_assert_data.line = 56;
__e_acsl_assert(__gen_e_acsl_p1_2,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
@@ -137,7 +143,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 = 52;
+ __gen_e_acsl_assert_data_2.line = 57;
__e_acsl_assert(__gen_e_acsl_p2_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
@@ -158,7 +164,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 = 53;
+ __gen_e_acsl_assert_data_3.line = 58;
__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_);
@@ -178,7 +184,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 = 55;
+ __gen_e_acsl_assert_data_4.line = 60;
__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);
}
@@ -200,7 +206,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 = 56;
+ __gen_e_acsl_assert_data_5.line = 61;
__e_acsl_assert(__gen_e_acsl_p2_6,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
}
@@ -226,7 +232,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 = 57;
+ __gen_e_acsl_assert_data_6.line = 62;
__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);
@@ -257,7 +263,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 = 58;
+ __gen_e_acsl_assert_data_7.line = 63;
__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);
@@ -283,7 +289,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 = 63;
+ __gen_e_acsl_assert_data_8.line = 68;
__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);
}
@@ -303,7 +309,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 = 66;
+ __gen_e_acsl_assert_data_9.line = 71;
__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);
@@ -324,7 +330,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 = 68;
+ __gen_e_acsl_assert_data_10.line = 73;
__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);
@@ -348,7 +354,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 = 73;
+ __gen_e_acsl_assert_data_11.line = 78;
__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);
}
@@ -369,7 +375,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 = 74;
+ __gen_e_acsl_assert_data_12.line = 79;
__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);
}
@@ -389,7 +395,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 = 79;
+ __gen_e_acsl_assert_data_13.line = 84;
__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);
}
@@ -406,7 +412,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 = 81;
+ __gen_e_acsl_assert_data_14.line = 86;
__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);
@@ -431,7 +437,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 = 83;
+ __gen_e_acsl_assert_data_15.line = 88;
__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);
@@ -450,7 +456,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 = 86;
+ __gen_e_acsl_assert_data_16.line = 90;
__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);
}
@@ -467,12 +473,29 @@ 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 = 87;
+ __gen_e_acsl_assert_data_17.line = 91;
__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);
}
/*@ assert f_here(27) == 27; */ ;
+ {
+ long __gen_e_acsl_f3_2;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data_18 =
+ {.values = (void *)0};
+ __gen_e_acsl_f3_2 = __gen_e_acsl_f3(5);
+ __e_acsl_assert_register_long(& __gen_e_acsl_assert_data_18,"f3(5)",0,
+ __gen_e_acsl_f3_2);
+ __gen_e_acsl_assert_data_18.blocking = 1;
+ __gen_e_acsl_assert_data_18.kind = "Assertion";
+ __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;
+ __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; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
@@ -741,4 +764,12 @@ void __gen_e_acsl_over(__e_acsl_mpq_t *__retres_arg, double a, double b)
return;
}
+/*@ assigns \result;
+ assigns \result \from y; */
+long __gen_e_acsl_f3(int y)
+{
+ long __retres = z + (long)y;
+ return __retres;
+}
+