diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index bbc74b118c622dbc23942b3409e8622ba3f86773..456f0e7d5234d24526ba4f326876639ec1f52e32 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -666,7 +666,7 @@ let rec type_term
ignore (type_term ~use_gmp_opt:true ~lenv li_t);
dup (type_term ~use_gmp_opt:true ?ctx ~lenv t).ty
| Tlambda ([ _ ],lt) ->
- dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx lt).ty;
+ dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx ~lenv lt).ty;
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index 802b5f343ad81eadb7468fc9e75cda1df8df18fe..428a12d2cb243e2d8963729e3579d9a52091f9bc 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -1,5 +1,6 @@
/* run.config
COMMENT: logic functions without labels
+ STDOPT: +"-eva-slevel 100"
*/
/*@ predicate p1(int x, int y) = x + y > 0; */
@@ -39,6 +40,9 @@ int glob = 5;
/*@ predicate p_notyet{L}(integer x) = x > 0; */
/*@ logic integer f_notyet{L}(integer x) = x; */
+// Test sums inside functions
+/*@ logic integer f_sum (integer x) = \sum(1,x,\lambda integer y; 1); */
+
int main(void) {
int x = 1, y = 2;
/*@ assert p1(x, y); */;
@@ -70,6 +74,8 @@ int main(void) {
double d = 2.0;
/*@ assert f2(d) > 0; */;
+ /*@ assert f_sum (100) == 100; */
+
// not yet supported
/* /\*@ assert p_notyet(27); *\/ ; */
/* /\*@ assert f_notyet(27) == 27; *\/ ; */
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 7e46c1c12dc7ceed37eea0767d07de1deba1e697..185e1121e6bf48381adef9c9c0aadfb859c57489 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,14 +1,15 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/functions.c:46: Warning:
+[eva:alarm] tests/arith/functions.c:50: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions.c:49: Warning:
+[eva:alarm] tests/arith/functions.c:53: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions.c:50: Warning:
+[eva:alarm] tests/arith/functions.c:54: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions.c:51: Warning:
+[eva:alarm] tests/arith/functions.c:55: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions.c:71: Warning:
+[eva:alarm] tests/arith/functions.c:75: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/arith/functions.c:71: Warning:
+[eva:alarm] tests/arith/functions.c:75: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/functions.c:77: 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 84bbc75c2b91cfd729292f295037c1e17932b0be..ea63da8c2d49f0623fc568027069a3e5c0abcc90 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -79,8 +79,12 @@ double __gen_e_acsl_f2(double x);
/*@ predicate p_notyet{L}(ℤ x) = x > 0;
*/
/*@ logic ℤ f_notyet{L}(ℤ x) = x;
+ */
+/*@ logic ℤ f_sum(ℤ x) = \sum(1, x, \lambda ℤ y; 1);
*/
+unsigned int __gen_e_acsl_f_sum(int x);
+
int main(void)
{
int __retres;
@@ -91,14 +95,14 @@ int main(void)
int __gen_e_acsl_p1_2;
__gen_e_acsl_p1_2 = __gen_e_acsl_p1(x,y);
__e_acsl_assert(__gen_e_acsl_p1_2,1,"Assertion","main","p1(x, y)",
- "tests/arith/functions.c",44);
+ "tests/arith/functions.c",48);
}
/*@ assert p1(x, y); */ ;
{
int __gen_e_acsl_p2_2;
__gen_e_acsl_p2_2 = __gen_e_acsl_p2(3,4);
__e_acsl_assert(__gen_e_acsl_p2_2,1,"Assertion","main","p2(3, 4)",
- "tests/arith/functions.c",45);
+ "tests/arith/functions.c",49);
}
/*@ assert p2(3, 4); */ ;
{
@@ -109,7 +113,7 @@ int main(void)
(__e_acsl_mpz_struct *)__gen_e_acsl_);
__e_acsl_assert(__gen_e_acsl_p2_4,1,"Assertion","main",
"p2(5, 99999999999999999999999999999)",
- "tests/arith/functions.c",46);
+ "tests/arith/functions.c",50);
__gmpz_clear(__gen_e_acsl_);
}
/*@ assert p2(5, 99999999999999999999999999999); */ ;
@@ -117,7 +121,7 @@ int main(void)
long __gen_e_acsl_f1_2;
__gen_e_acsl_f1_2 = __gen_e_acsl_f1(x,y);
__e_acsl_assert(__gen_e_acsl_f1_2 == 3L,1,"Assertion","main",
- "f1(x, y) == 3","tests/arith/functions.c",48);
+ "f1(x, y) == 3","tests/arith/functions.c",52);
}
/*@ assert f1(x, y) ≡ 3; */ ;
{
@@ -126,7 +130,7 @@ int main(void)
__gen_e_acsl_f1_4 = __gen_e_acsl_f1(3,4);
__gen_e_acsl_p2_6 = __gen_e_acsl_p2_5(x,__gen_e_acsl_f1_4);
__e_acsl_assert(__gen_e_acsl_p2_6,1,"Assertion","main","p2(x, f1(3, 4))",
- "tests/arith/functions.c",49);
+ "tests/arith/functions.c",53);
}
/*@ assert p2(x, f1(3, 4)); */ ;
{
@@ -142,7 +146,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__5));
__e_acsl_assert(__gen_e_acsl_gt_3 > 0,1,"Assertion","main",
"f1(9, 99999999999999999999999999999) > 0",
- "tests/arith/functions.c",50);
+ "tests/arith/functions.c",54);
__gmpz_clear(__gen_e_acsl__4);
__gmpz_clear(__gen_e_acsl_f1_6);
__gmpz_clear(__gen_e_acsl__5);
@@ -162,7 +166,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main",
"f1(99999999999999999999999999999, 99999999999999999999999999999) ==\n199999999999999999999999999998",
- "tests/arith/functions.c",51);
+ "tests/arith/functions.c",55);
__gmpz_clear(__gen_e_acsl__6);
__gmpz_clear(__gen_e_acsl_f1_8);
__gmpz_clear(__gen_e_acsl__7);
@@ -176,7 +180,7 @@ int main(void)
int __gen_e_acsl_g_2;
__gen_e_acsl_g_2 = __gen_e_acsl_g(x);
__e_acsl_assert(__gen_e_acsl_g_2 == x,1,"Assertion","main","g(x) == x",
- "tests/arith/functions.c",56);
+ "tests/arith/functions.c",60);
}
/*@ assert g(x) ≡ x; */ ;
char c = (char)'c';
@@ -184,7 +188,7 @@ int main(void)
int __gen_e_acsl_h_char_2;
__gen_e_acsl_h_char_2 = __gen_e_acsl_h_char((int)c);
__e_acsl_assert(__gen_e_acsl_h_char_2 == (int)c,1,"Assertion","main",
- "h_char(c) == c","tests/arith/functions.c",59);
+ "h_char(c) == c","tests/arith/functions.c",63);
}
/*@ assert h_char(c) ≡ c; */ ;
short s = (short)1;
@@ -192,7 +196,7 @@ int main(void)
int __gen_e_acsl_h_short_2;
__gen_e_acsl_h_short_2 = __gen_e_acsl_h_short((int)s);
__e_acsl_assert(__gen_e_acsl_h_short_2 == (int)s,1,"Assertion","main",
- "h_short(s) == s","tests/arith/functions.c",61);
+ "h_short(s) == s","tests/arith/functions.c",65);
}
/*@ assert h_short(s) ≡ s; */ ;
m.k = 8;
@@ -203,7 +207,7 @@ int main(void)
__gen_e_acsl_t1_2 = __gen_e_acsl_t1(m);
__gen_e_acsl_t2_2 = __gen_e_acsl_t2(__gen_e_acsl_t1_2);
__e_acsl_assert(__gen_e_acsl_t2_2 == 17L,1,"Assertion","main",
- "t2(t1(m)) == 17","tests/arith/functions.c",66);
+ "t2(t1(m)) == 17","tests/arith/functions.c",70);
}
/*@ assert t2(t1(m)) ≡ 17; */ ;
__gen_e_acsl_k(9);
@@ -212,9 +216,16 @@ int main(void)
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.,1,"Assertion","main","f2(d) > 0",
- "tests/arith/functions.c",71);
+ "tests/arith/functions.c",75);
}
/*@ assert f2(d) > 0; */ ;
+ {
+ unsigned int __gen_e_acsl_f_sum_2;
+ __gen_e_acsl_f_sum_2 = __gen_e_acsl_f_sum(100);
+ __e_acsl_assert(__gen_e_acsl_f_sum_2 == 100U,1,"Assertion","main",
+ "f_sum(100) == 100","tests/arith/functions.c",77);
+ }
+ /*@ assert f_sum(100) ≡ 100; */ ;
__retres = 0;
return __retres;
}
@@ -226,7 +237,7 @@ void __gen_e_acsl_k(int x)
int __gen_e_acsl_k_pred_2;
__gen_e_acsl_k_pred_2 = __gen_e_acsl_k_pred(x);
__e_acsl_assert(__gen_e_acsl_k_pred_2,1,"Precondition","k","k_pred(x)",
- "tests/arith/functions.c",27);
+ "tests/arith/functions.c",28);
}
k(x);
return;
@@ -417,4 +428,30 @@ double __gen_e_acsl_f2(double x)
return __gen_e_acsl__10;
}
+/*@ assigns \result;
+ assigns \result \from x; */
+unsigned int __gen_e_acsl_f_sum(int x)
+{
+ long __gen_e_acsl_y_2;
+ long __gen_e_acsl_one;
+ int __gen_e_acsl_cond;
+ unsigned int __gen_e_acsl_lambda;
+ unsigned int __gen_e_acsl_accumulator;
+ __gen_e_acsl_one = 1;
+ __gen_e_acsl_cond = 0;
+ __gen_e_acsl_lambda = 0;
+ __gen_e_acsl_accumulator = 0;
+ __gen_e_acsl_y_2 = 1L;
+ while (1) {
+ __gen_e_acsl_cond = __gen_e_acsl_y_2 > (long)x;
+ if (__gen_e_acsl_cond) break;
+ else {
+ __gen_e_acsl_lambda = 1;
+ __gen_e_acsl_accumulator += __gen_e_acsl_lambda;
+ __gen_e_acsl_y_2 += __gen_e_acsl_one;
+ }
+ }
+ return __gen_e_acsl_accumulator;
+}
+