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 bd14370f572710c15132e2d91dabb069a4ff9fc3..dc51dcaf62a26dfaa493d6061af5d7f4c135475e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
@@ -80,8 +80,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;
@@ -92,14 +96,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); */ ;
{
@@ -110,7 +114,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); */ ;
@@ -118,7 +122,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; */ ;
{
@@ -127,7 +131,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)); */ ;
{
@@ -143,7 +147,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);
@@ -163,7 +167,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);
@@ -177,7 +181,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';
@@ -185,7 +189,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;
@@ -193,7 +197,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;
@@ -204,7 +208,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);
@@ -213,9 +217,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;
}
@@ -227,7 +238,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;
@@ -418,4 +429,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;
+}
+
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
index 762933f8fed7f20ae90e68b8b016ae87026769b0..e0b0c88196bc2999ad0b71823873a96b033e8fa1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -197,14 +197,76 @@ int main(void)
x % 2 ≡ 0 ⇒ (∃ ℤ y; 0 ≤ y ≤ x / 2 ∧ x ≡ 2 * y);
*/
;
+ {
+ int __gen_e_acsl_forall_6;
+ int __gen_e_acsl_x_7;
+ __gen_e_acsl_forall_6 = 1;
+ __gen_e_acsl_x_7 = 0;
+ while (1) {
+ if (__gen_e_acsl_x_7 < 10) ; else break;
+ {
+ int __gen_e_acsl_forall_7;
+ int __gen_e_acsl_y_3;
+ int __gen_e_acsl_and;
+ __gen_e_acsl_forall_7 = 1;
+ __gen_e_acsl_y_3 = 10;
+ while (1) {
+ if (__gen_e_acsl_y_3 < 20) ; else break;
+ if (__gen_e_acsl_x_7 <= __gen_e_acsl_y_3) ;
+ else {
+ __gen_e_acsl_forall_7 = 0;
+ goto e_acsl_end_loop8;
+ }
+ __gen_e_acsl_y_3 ++;
+ }
+ e_acsl_end_loop8: ;
+ if (__gen_e_acsl_forall_7) {
+ int __gen_e_acsl_forall_8;
+ int __gen_e_acsl_y_4;
+ __gen_e_acsl_forall_8 = 1;
+ __gen_e_acsl_y_4 = -10;
+ while (1) {
+ if (__gen_e_acsl_y_4 < 0) ; else break;
+ if (__gen_e_acsl_y_4 <= __gen_e_acsl_x_7) ;
+ else {
+ __gen_e_acsl_forall_8 = 0;
+ goto e_acsl_end_loop9;
+ }
+ __gen_e_acsl_y_4 ++;
+ }
+ e_acsl_end_loop9: ;
+ __gen_e_acsl_and = __gen_e_acsl_forall_8;
+ }
+ else __gen_e_acsl_and = 0;
+ if (__gen_e_acsl_and) ;
+ else {
+ __gen_e_acsl_forall_6 = 0;
+ goto e_acsl_end_loop10;
+ }
+ }
+ __gen_e_acsl_x_7 ++;
+ }
+ e_acsl_end_loop10: ;
+ __e_acsl_assert(__gen_e_acsl_forall_6,1,"Assertion","main",
+ "\\forall int x;\n 0 <= x < 10 ==>\n (\\forall int y; 10 <= y < 20 ==> x <= y) &&\n (\\forall int y; -10 <= y < 0 ==> y <= x)",
+ "tests/arith/quantif.i",36);
+ }
+ /*@
+ assert
+ ∀ int x;
+ 0 ≤ x < 10 ⇒
+ (∀ int y; 10 ≤ y < 20 ⇒ x ≤ y) ∧
+ (∀ int y; -10 ≤ y < 0 ⇒ y ≤ x);
+ */
+ ;
{
int buf[10];
__e_acsl_store_block((void *)(buf),(size_t)40);
unsigned long len = (unsigned long)9;
{
- int __gen_e_acsl_forall_6;
+ int __gen_e_acsl_forall_9;
int __gen_e_acsl_i;
- __gen_e_acsl_forall_6 = 1;
+ __gen_e_acsl_forall_9 = 1;
__gen_e_acsl_i = 0;
while (1) {
if (__gen_e_acsl_i < 10) ; else break;
@@ -215,22 +277,22 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid) ;
else {
- __gen_e_acsl_forall_6 = 0;
- goto e_acsl_end_loop8;
+ __gen_e_acsl_forall_9 = 0;
+ goto e_acsl_end_loop11;
}
}
__gen_e_acsl_i ++;
}
- e_acsl_end_loop8: ;
- __e_acsl_assert(__gen_e_acsl_forall_6,1,"Assertion","main",
+ e_acsl_end_loop11: ;
+ __e_acsl_assert(__gen_e_acsl_forall_9,1,"Assertion","main",
"\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])",
- "tests/arith/quantif.i",37);
+ "tests/arith/quantif.i",43);
}
/*@ assert ∀ ℤ i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */ ;
{
- int __gen_e_acsl_forall_7;
+ int __gen_e_acsl_forall_10;
int __gen_e_acsl_i_2;
- __gen_e_acsl_forall_7 = 1;
+ __gen_e_acsl_forall_10 = 1;
__gen_e_acsl_i_2 = (char)0;
while (1) {
if (__gen_e_acsl_i_2 < 10) ; else break;
@@ -241,22 +303,22 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_2) ;
else {
- __gen_e_acsl_forall_7 = 0;
- goto e_acsl_end_loop9;
+ __gen_e_acsl_forall_10 = 0;
+ goto e_acsl_end_loop12;
}
}
__gen_e_acsl_i_2 ++;
}
- e_acsl_end_loop9: ;
- __e_acsl_assert(__gen_e_acsl_forall_7,1,"Assertion","main",
+ e_acsl_end_loop12: ;
+ __e_acsl_assert(__gen_e_acsl_forall_10,1,"Assertion","main",
"\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])",
- "tests/arith/quantif.i",38);
+ "tests/arith/quantif.i",44);
}
/*@ assert ∀ char i; 0 ≤ i < 10 ⇒ \valid(&buf[i]); */ ;
{
- int __gen_e_acsl_forall_8;
+ int __gen_e_acsl_forall_11;
unsigned long __gen_e_acsl_i_3;
- __gen_e_acsl_forall_8 = 1;
+ __gen_e_acsl_forall_11 = 1;
__gen_e_acsl_i_3 = 0UL;
while (1) {
if (__gen_e_acsl_i_3 < len) ; else break;
@@ -267,22 +329,22 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_3) ;
else {
- __gen_e_acsl_forall_8 = 0;
- goto e_acsl_end_loop10;
+ __gen_e_acsl_forall_11 = 0;
+ goto e_acsl_end_loop13;
}
}
__gen_e_acsl_i_3 ++;
}
- e_acsl_end_loop10: ;
- __e_acsl_assert(__gen_e_acsl_forall_8,1,"Assertion","main",
+ e_acsl_end_loop13: ;
+ __e_acsl_assert(__gen_e_acsl_forall_11,1,"Assertion","main",
"\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])",
- "tests/arith/quantif.i",39);
+ "tests/arith/quantif.i",45);
}
/*@ assert ∀ ℤ i; 0 ≤ i < len ⇒ \valid(&buf[i]); */ ;
{
- int __gen_e_acsl_forall_9;
+ int __gen_e_acsl_forall_12;
__e_acsl_mpz_t __gen_e_acsl_i_4;
- __gen_e_acsl_forall_9 = 1;
+ __gen_e_acsl_forall_12 = 1;
__gmpz_init(__gen_e_acsl_i_4);
{
__e_acsl_mpz_t __gen_e_acsl_;
@@ -310,8 +372,8 @@ int main(void)
(void *)0);
if (__gen_e_acsl_valid_4) ;
else {
- __gen_e_acsl_forall_9 = 0;
- goto e_acsl_end_loop11;
+ __gen_e_acsl_forall_12 = 0;
+ goto e_acsl_end_loop14;
}
}
{
@@ -328,10 +390,10 @@ int main(void)
__gmpz_clear(__gen_e_acsl_add);
}
}
- e_acsl_end_loop11: ;
- __e_acsl_assert(__gen_e_acsl_forall_9,1,"Assertion","main",
+ e_acsl_end_loop14: ;
+ __e_acsl_assert(__gen_e_acsl_forall_12,1,"Assertion","main",
"\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])",
- "tests/arith/quantif.i",40);
+ "tests/arith/quantif.i",46);
__gmpz_clear(__gen_e_acsl_i_4);
}
/*@ assert ∀ ℤ i; 0 ≤ i ≤ len ⇒ \valid(&buf[i]); */ ;
@@ -339,29 +401,29 @@ int main(void)
}
__e_acsl_assert(1,1,"Assertion","main",
"\\forall integer x; 0 < x < 1 ==> \\false",
- "tests/arith/quantif.i",44);
+ "tests/arith/quantif.i",50);
/*@ assert ∀ ℤ x; 0 < x < 1 ⇒ \false; */ ;
__e_acsl_assert(! 0,1,"Assertion","main",
"!(\\exists char c; 10 <= c < 10 && c == 10)",
- "tests/arith/quantif.i",45);
+ "tests/arith/quantif.i",51);
/*@ assert ¬(∃ char c; 10 ≤ c < 10 ∧ c ≡ 10); */ ;
{
int __gen_e_acsl_u;
__gen_e_acsl_u = 5;
__e_acsl_assert(1,1,"Assertion","main",
"\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false",
- "tests/arith/quantif.i",47);
+ "tests/arith/quantif.i",53);
}
/*@
assert \let u = 5; ∀ ℤ x, ℤ y; 0 ≤ x < 2 ∧ 4 < y < u ⇒ \false;
*/
;
{
- int __gen_e_acsl_forall_10;
+ int __gen_e_acsl_forall_13;
int __gen_e_acsl_i_6;
int __gen_e_acsl_j;
int __gen_e_acsl_k;
- __gen_e_acsl_forall_10 = 1;
+ __gen_e_acsl_forall_13 = 1;
__gen_e_acsl_i_6 = 0;
while (1) {
if (__gen_e_acsl_i_6 < 10) ; else break;
@@ -378,8 +440,8 @@ int main(void)
__gen_e_acsl_k);
if (__gen_e_acsl_p1_2) ;
else {
- __gen_e_acsl_forall_10 = 0;
- goto e_acsl_end_loop12;
+ __gen_e_acsl_forall_13 = 0;
+ goto e_acsl_end_loop15;
}
}
__gen_e_acsl_k ++;
@@ -388,10 +450,10 @@ int main(void)
}
__gen_e_acsl_i_6 ++;
}
- e_acsl_end_loop12: ;
- __e_acsl_assert(__gen_e_acsl_forall_10,1,"Assertion","main",
+ e_acsl_end_loop15: ;
+ __e_acsl_assert(__gen_e_acsl_forall_13,1,"Assertion","main",
"forall_multiple_binders_1:\n \\forall integer i, integer j, integer k;\n 0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12 ==> p1(i, j, k)",
- "tests/arith/quantif.i",53);
+ "tests/arith/quantif.i",59);
}
/*@
assert
@@ -401,11 +463,11 @@ int main(void)
*/
;
{
- int __gen_e_acsl_forall_11;
+ int __gen_e_acsl_forall_14;
int __gen_e_acsl_i_7;
int __gen_e_acsl_j_2;
int __gen_e_acsl_k_2;
- __gen_e_acsl_forall_11 = 1;
+ __gen_e_acsl_forall_14 = 1;
__gen_e_acsl_i_7 = 0;
while (1) {
if (__gen_e_acsl_i_7 < 10) ; else break;
@@ -422,8 +484,8 @@ int main(void)
__gen_e_acsl_k_2);
if (__gen_e_acsl_p2_2) ;
else {
- __gen_e_acsl_forall_11 = 0;
- goto e_acsl_end_loop13;
+ __gen_e_acsl_forall_14 = 0;
+ goto e_acsl_end_loop16;
}
}
__gen_e_acsl_k_2 ++;
@@ -432,10 +494,10 @@ int main(void)
}
__gen_e_acsl_i_7 ++;
}
- e_acsl_end_loop13: ;
- __e_acsl_assert(__gen_e_acsl_forall_11,1,"Assertion","main",
+ e_acsl_end_loop16: ;
+ __e_acsl_assert(__gen_e_acsl_forall_14,1,"Assertion","main",
"forall_multiple_binders_2:\n \\forall integer i, integer j, integer k;\n 0 <= i <= j < k <= 10 ==> p2(i, j, k)",
- "tests/arith/quantif.i",56);
+ "tests/arith/quantif.i",62);
}
/*@
assert
@@ -444,11 +506,11 @@ int main(void)
*/
;
{
- int __gen_e_acsl_forall_12;
+ int __gen_e_acsl_forall_15;
int __gen_e_acsl_i_8;
int __gen_e_acsl_j_3;
int __gen_e_acsl_k_3;
- __gen_e_acsl_forall_12 = 1;
+ __gen_e_acsl_forall_15 = 1;
__gen_e_acsl_i_8 = 0;
while (1) {
if (__gen_e_acsl_i_8 < 10) ; else break;
@@ -465,8 +527,8 @@ int main(void)
__gen_e_acsl_k_3);
if (__gen_e_acsl_p3_2) ;
else {
- __gen_e_acsl_forall_12 = 0;
- goto e_acsl_end_loop14;
+ __gen_e_acsl_forall_15 = 0;
+ goto e_acsl_end_loop17;
}
}
__gen_e_acsl_k_3 ++;
@@ -475,10 +537,10 @@ int main(void)
}
__gen_e_acsl_i_8 ++;
}
- e_acsl_end_loop14: ;
- __e_acsl_assert(__gen_e_acsl_forall_12,1,"Assertion","main",
+ e_acsl_end_loop17: ;
+ __e_acsl_assert(__gen_e_acsl_forall_15,1,"Assertion","main",
"forall_multiple_binders_3:\n \\forall integer i, integer j, integer k;\n 0 <= i < j <= 10 && 1 < k < 11 ==> p3(i, j, k)",
- "tests/arith/quantif.i",59);
+ "tests/arith/quantif.i",65);
}
/*@
assert
@@ -488,11 +550,11 @@ int main(void)
*/
;
{
- int __gen_e_acsl_forall_13;
+ int __gen_e_acsl_forall_16;
int __gen_e_acsl_i_9;
int __gen_e_acsl_j_4;
int __gen_e_acsl_k_4;
- __gen_e_acsl_forall_13 = 1;
+ __gen_e_acsl_forall_16 = 1;
__gen_e_acsl_i_9 = 0;
while (1) {
if (__gen_e_acsl_i_9 < 10) ; else break;
@@ -509,8 +571,8 @@ int main(void)
__gen_e_acsl_k_4);
if (__gen_e_acsl_p1_4) ;
else {
- __gen_e_acsl_forall_13 = 0;
- goto e_acsl_end_loop15;
+ __gen_e_acsl_forall_16 = 0;
+ goto e_acsl_end_loop18;
}
}
__gen_e_acsl_k_4 ++;
@@ -519,10 +581,10 @@ int main(void)
}
__gen_e_acsl_i_9 ++;
}
- e_acsl_end_loop15: ;
- __e_acsl_assert(__gen_e_acsl_forall_13,1,"Assertion","main",
+ e_acsl_end_loop18: ;
+ __e_acsl_assert(__gen_e_acsl_forall_16,1,"Assertion","main",
"forall_multiple_binders_4:\n \\forall integer i, integer j, integer k;\n 0 <= i < 10 ==> 1 < j <= 11 ==> 2 <= k <= 12 ==> p1(i, j, k)",
- "tests/arith/quantif.i",62);
+ "tests/arith/quantif.i",68);
}
/*@
assert
@@ -532,11 +594,11 @@ int main(void)
*/
;
{
- int __gen_e_acsl_forall_14;
+ int __gen_e_acsl_forall_17;
int __gen_e_acsl_i_10;
int __gen_e_acsl_k_5;
int __gen_e_acsl_j_5;
- __gen_e_acsl_forall_14 = 1;
+ __gen_e_acsl_forall_17 = 1;
__gen_e_acsl_i_10 = 0;
while (1) {
if (__gen_e_acsl_i_10 <= 10) ; else break;
@@ -553,8 +615,8 @@ int main(void)
__gen_e_acsl_k_5);
if (__gen_e_acsl_p4_2) ;
else {
- __gen_e_acsl_forall_14 = 0;
- goto e_acsl_end_loop16;
+ __gen_e_acsl_forall_17 = 0;
+ goto e_acsl_end_loop19;
}
}
__gen_e_acsl_j_5 ++;
@@ -563,10 +625,10 @@ int main(void)
}
__gen_e_acsl_i_10 ++;
}
- e_acsl_end_loop16: ;
- __e_acsl_assert(__gen_e_acsl_forall_14,1,"Assertion","main",
+ e_acsl_end_loop19: ;
+ __e_acsl_assert(__gen_e_acsl_forall_17,1,"Assertion","main",
"forall_unordered_binders:\n \\forall integer i, integer j, integer k;\n 0 <= i <= k <= 10 && 1 <= j < k ==> p4(i, j, k)",
- "tests/arith/quantif.i",65);
+ "tests/arith/quantif.i",71);
}
/*@
assert
@@ -598,7 +660,7 @@ int main(void)
if (! __gen_e_acsl_p1_6) ;
else {
__gen_e_acsl_exists_3 = 1;
- goto e_acsl_end_loop17;
+ goto e_acsl_end_loop20;
}
}
__gen_e_acsl_k_6 ++;
@@ -607,10 +669,10 @@ int main(void)
}
__gen_e_acsl_i_11 ++;
}
- e_acsl_end_loop17: ;
+ e_acsl_end_loop20: ;
__e_acsl_assert(__gen_e_acsl_exists_3,1,"Assertion","main",
"exists_multiple_binders_1:\n \\exists integer i, integer j, integer k;\n 0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12 && p1(i, j, k)",
- "tests/arith/quantif.i",68);
+ "tests/arith/quantif.i",74);
}
/*@
assert
@@ -642,7 +704,7 @@ int main(void)
if (! __gen_e_acsl_p2_4) ;
else {
__gen_e_acsl_exists_4 = 1;
- goto e_acsl_end_loop18;
+ goto e_acsl_end_loop21;
}
}
__gen_e_acsl_k_7 ++;
@@ -651,10 +713,10 @@ int main(void)
}
__gen_e_acsl_i_12 ++;
}
- e_acsl_end_loop18: ;
+ e_acsl_end_loop21: ;
__e_acsl_assert(__gen_e_acsl_exists_4,1,"Assertion","main",
"exists_multiple_binders_2:\n \\exists integer i, integer j, integer k;\n 0 <= i <= j < k <= 10 && p2(i, j, k)",
- "tests/arith/quantif.i",71);
+ "tests/arith/quantif.i",77);
}
/*@
assert
@@ -685,7 +747,7 @@ int main(void)
if (! __gen_e_acsl_p3_4) ;
else {
__gen_e_acsl_exists_5 = 1;
- goto e_acsl_end_loop19;
+ goto e_acsl_end_loop22;
}
}
__gen_e_acsl_k_8 ++;
@@ -694,10 +756,10 @@ int main(void)
}
__gen_e_acsl_i_13 ++;
}
- e_acsl_end_loop19: ;
+ e_acsl_end_loop22: ;
__e_acsl_assert(__gen_e_acsl_exists_5,1,"Assertion","main",
"exists_multiple_binders_3:\n \\exists integer i, integer j, integer k;\n 0 <= i < j <= 10 && 1 < k < 11 && p3(i, j, k)",
- "tests/arith/quantif.i",74);
+ "tests/arith/quantif.i",80);
}
/*@
assert
@@ -729,7 +791,7 @@ int main(void)
if (! __gen_e_acsl_p4_4) ;
else {
__gen_e_acsl_exists_6 = 1;
- goto e_acsl_end_loop20;
+ goto e_acsl_end_loop23;
}
}
__gen_e_acsl_j_9 ++;
@@ -738,10 +800,10 @@ int main(void)
}
__gen_e_acsl_i_14 ++;
}
- e_acsl_end_loop20: ;
+ e_acsl_end_loop23: ;
__e_acsl_assert(__gen_e_acsl_exists_6,1,"Assertion","main",
"exists_unordered_binders:\n \\exists integer i, integer j, integer k;\n 0 <= i <= k <= 10 && 1 <= j < k && p4(i, j, k)",
- "tests/arith/quantif.i",77);
+ "tests/arith/quantif.i",83);
}
/*@
assert
@@ -815,72 +877,72 @@ int main(void)
assigns \result \from i, j, k; */
int __gen_e_acsl_p1(int i, int j, int k)
{
- int __gen_e_acsl_and;
int __gen_e_acsl_and_2;
int __gen_e_acsl_and_3;
int __gen_e_acsl_and_4;
int __gen_e_acsl_and_5;
- if (0 <= i) __gen_e_acsl_and = i < 10; else __gen_e_acsl_and = 0;
- if (__gen_e_acsl_and) __gen_e_acsl_and_2 = 1 < j;
- else __gen_e_acsl_and_2 = 0;
- if (__gen_e_acsl_and_2) __gen_e_acsl_and_3 = j <= 11;
+ int __gen_e_acsl_and_6;
+ if (0 <= i) __gen_e_acsl_and_2 = i < 10; else __gen_e_acsl_and_2 = 0;
+ if (__gen_e_acsl_and_2) __gen_e_acsl_and_3 = 1 < j;
else __gen_e_acsl_and_3 = 0;
- if (__gen_e_acsl_and_3) __gen_e_acsl_and_4 = 2 <= k;
+ if (__gen_e_acsl_and_3) __gen_e_acsl_and_4 = j <= 11;
else __gen_e_acsl_and_4 = 0;
- if (__gen_e_acsl_and_4) __gen_e_acsl_and_5 = k <= 12;
+ if (__gen_e_acsl_and_4) __gen_e_acsl_and_5 = 2 <= k;
else __gen_e_acsl_and_5 = 0;
- return __gen_e_acsl_and_5;
+ if (__gen_e_acsl_and_5) __gen_e_acsl_and_6 = k <= 12;
+ else __gen_e_acsl_and_6 = 0;
+ return __gen_e_acsl_and_6;
}
/*@ assigns \result;
assigns \result \from i, j, k; */
int __gen_e_acsl_p2(int i, int j, int k)
{
- int __gen_e_acsl_and_6;
int __gen_e_acsl_and_7;
int __gen_e_acsl_and_8;
- if (0 <= i) __gen_e_acsl_and_6 = i <= j; else __gen_e_acsl_and_6 = 0;
- if (__gen_e_acsl_and_6) __gen_e_acsl_and_7 = j < k;
- else __gen_e_acsl_and_7 = 0;
- if (__gen_e_acsl_and_7) __gen_e_acsl_and_8 = k <= 10;
+ int __gen_e_acsl_and_9;
+ if (0 <= i) __gen_e_acsl_and_7 = i <= j; else __gen_e_acsl_and_7 = 0;
+ if (__gen_e_acsl_and_7) __gen_e_acsl_and_8 = j < k;
else __gen_e_acsl_and_8 = 0;
- return __gen_e_acsl_and_8;
+ if (__gen_e_acsl_and_8) __gen_e_acsl_and_9 = k <= 10;
+ else __gen_e_acsl_and_9 = 0;
+ return __gen_e_acsl_and_9;
}
/*@ assigns \result;
assigns \result \from i, j, k; */
int __gen_e_acsl_p3(int i, int j, int k)
{
- int __gen_e_acsl_and_9;
int __gen_e_acsl_and_10;
int __gen_e_acsl_and_11;
int __gen_e_acsl_and_12;
- if (0 <= i) __gen_e_acsl_and_9 = i < j; else __gen_e_acsl_and_9 = 0;
- if (__gen_e_acsl_and_9) __gen_e_acsl_and_10 = j <= 10;
- else __gen_e_acsl_and_10 = 0;
- if (__gen_e_acsl_and_10) __gen_e_acsl_and_11 = 1 < k;
+ int __gen_e_acsl_and_13;
+ if (0 <= i) __gen_e_acsl_and_10 = i < j; else __gen_e_acsl_and_10 = 0;
+ if (__gen_e_acsl_and_10) __gen_e_acsl_and_11 = j <= 10;
else __gen_e_acsl_and_11 = 0;
- if (__gen_e_acsl_and_11) __gen_e_acsl_and_12 = k < 11;
+ if (__gen_e_acsl_and_11) __gen_e_acsl_and_12 = 1 < k;
else __gen_e_acsl_and_12 = 0;
- return __gen_e_acsl_and_12;
+ if (__gen_e_acsl_and_12) __gen_e_acsl_and_13 = k < 11;
+ else __gen_e_acsl_and_13 = 0;
+ return __gen_e_acsl_and_13;
}
/*@ assigns \result;
assigns \result \from i, j, k; */
int __gen_e_acsl_p4(int i, int j, int k)
{
- int __gen_e_acsl_and_13;
int __gen_e_acsl_and_14;
int __gen_e_acsl_and_15;
int __gen_e_acsl_and_16;
- if (0 <= i) __gen_e_acsl_and_13 = i <= k; else __gen_e_acsl_and_13 = 0;
- if (__gen_e_acsl_and_13) __gen_e_acsl_and_14 = k <= 10;
- else __gen_e_acsl_and_14 = 0;
- if (__gen_e_acsl_and_14) __gen_e_acsl_and_15 = 1 <= j;
+ int __gen_e_acsl_and_17;
+ if (0 <= i) __gen_e_acsl_and_14 = i <= k; else __gen_e_acsl_and_14 = 0;
+ if (__gen_e_acsl_and_14) __gen_e_acsl_and_15 = k <= 10;
else __gen_e_acsl_and_15 = 0;
- if (__gen_e_acsl_and_15) __gen_e_acsl_and_16 = j < k;
+ if (__gen_e_acsl_and_15) __gen_e_acsl_and_16 = 1 <= j;
else __gen_e_acsl_and_16 = 0;
- return __gen_e_acsl_and_16;
+ if (__gen_e_acsl_and_16) __gen_e_acsl_and_17 = j < k;
+ else __gen_e_acsl_and_17 = 0;
+ return __gen_e_acsl_and_17;
}
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
index b588f0c95ed7b1de91e82f1a165dd0d2426674c3..2eaa50601e582586894367106078a8ef630d85eb 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
@@ -1,67 +1,67 @@
[e-acsl] beginning translation.
-[e-acsl] tests/arith/quantif.i:82: Warning:
+[e-acsl] tests/arith/quantif.i:88: Warning:
invalid E-ACSL construct
`invalid guard 10 > i in quantification
failed_invalid_guards: ∀ ℤ i; 10 > i ≥ 0 ⇒ p1(i, 2, 2).
Missing guard for i. Only < and ≤ are allowed to guard quantifier variables'.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:84: Warning:
+[e-acsl] tests/arith/quantif.i:90: Warning:
invalid E-ACSL construct
`invalid guard p1(i, j, k) in quantification
failed_unguarded_k:
∀ ℤ i, ℤ j, ℤ k; 0 ≤ i < 10 ∧ 1 < j ≤ 11 ⇒ p1(i, j, k).
Missing guard for k. '.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:86: Warning:
+[e-acsl] tests/arith/quantif.i:92: Warning:
E-ACSL construct
`non integer variable i in quantification
failed_non_integer: ∀ ℠i; 0 ≤ i < 10 ⇒ p1(\truncate(i), 2, 2)'
is not yet supported.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:88: Warning:
+[e-acsl] tests/arith/quantif.i:94: Warning:
invalid E-ACSL construct
`missing lower bound for i in quantification
failed_missing_lower_bound: ∀ ℤ i; i < 10 ⇒ p1(i, 2, 2)'.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:90: Warning:
+[e-acsl] tests/arith/quantif.i:96: Warning:
invalid E-ACSL construct
`invalid guard p1(i, 2, 2) in quantification
failded_missing_upper_bound: ∀ ℤ i; 0 ≤ i ⇒ p1(i, 2, 2).
Missing upper bound for i. '.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:92: Warning:
+[e-acsl] tests/arith/quantif.i:98: Warning:
invalid E-ACSL construct
`invalid guard p1(i, j, 2) in quantification
failed_invalid_upper_bound_1: ∀ ℤ i, ℤ j; 0 ≤ i < j ⇒ p1(i, j, 2).
Missing upper bound for j. '.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:94: Warning:
+[e-acsl] tests/arith/quantif.i:100: Warning:
invalid E-ACSL construct
`missing lower bound for i when processing the linked upper bound i < j
in quantification
failed_invalid_upper_bound_2:
∀ ℤ i, ℤ j; i < j ∧ 0 ≤ i ⇒ p1(i, 2, 2)'.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:96: Warning:
+[e-acsl] tests/arith/quantif.i:102: Warning:
invalid E-ACSL construct
`found existing lower bound i < j when processing 3 ≤ j in quantification
failed_extra_constraint:
∀ ℤ i, ℤ j; 0 ≤ i < j ∧ i < 10 ∧ 3 ≤ j < 5 ⇒ p1(i, j, 2)'.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:98: Warning:
+[e-acsl] tests/arith/quantif.i:104: Warning:
invalid E-ACSL construct
`found existing lower bound 0 ≤ i when processing j < i in quantification
failed_multiple_upper_bounds:
∀ ℤ i, ℤ j; 0 ≤ i < j < i ∧ j ≤ 10 ⇒ p1(i, j, 2)'.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:100: Warning:
+[e-acsl] tests/arith/quantif.i:106: Warning:
invalid E-ACSL construct
`found existing lower bound i < k when processing j < k in quantification
multiple_linked_upper:
∀ ℤ i, ℤ j, ℤ k;
0 ≤ i < k ∧ 1 ≤ j < k ∧ 2 ≤ k < 10 ⇒ p1(i, j, k)'.
Ignoring annotation.
-[e-acsl] tests/arith/quantif.i:102: Warning:
+[e-acsl] tests/arith/quantif.i:108: Warning:
invalid E-ACSL construct
`invalid constraint 2 ≤ i, both operands are constants or already bounded in quantification
multiple_guard:
@@ -71,34 +71,34 @@
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/arith/quantif.i:22: Warning: assertion got status unknown.
[eva:alarm] tests/arith/quantif.i:31: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:40: Warning:
+[eva:alarm] tests/arith/quantif.i:46: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/quantif.i:47: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/quantif.i:56: Warning:
+[eva:alarm] tests/arith/quantif.i:53: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:62: Warning:
assertion 'forall_multiple_binders_2' got status unknown.
-[eva:alarm] tests/arith/quantif.i:59: Warning:
- assertion 'forall_multiple_binders_3' got status unknown.
[eva:alarm] tests/arith/quantif.i:65: Warning:
- assertion 'forall_unordered_binders' got status unknown.
+ assertion 'forall_multiple_binders_3' got status unknown.
[eva:alarm] tests/arith/quantif.i:71: Warning:
+ assertion 'forall_unordered_binders' got status unknown.
+[eva:alarm] tests/arith/quantif.i:77: Warning:
assertion 'exists_multiple_binders_2' got status unknown.
-[eva:alarm] tests/arith/quantif.i:74: Warning:
+[eva:alarm] tests/arith/quantif.i:80: Warning:
assertion 'exists_multiple_binders_3' got status unknown.
-[eva:alarm] tests/arith/quantif.i:77: Warning:
+[eva:alarm] tests/arith/quantif.i:83: Warning:
assertion 'exists_unordered_binders' got status unknown.
-[eva:alarm] tests/arith/quantif.i:84: Warning:
+[eva:alarm] tests/arith/quantif.i:90: Warning:
assertion 'failed_unguarded_k' got status unknown.
-[eva:alarm] tests/arith/quantif.i:86: Warning:
+[eva:alarm] tests/arith/quantif.i:92: Warning:
assertion 'failed_non_integer' got status unknown.
-[eva:alarm] tests/arith/quantif.i:88: Warning:
+[eva:alarm] tests/arith/quantif.i:94: Warning:
assertion 'failed_missing_lower_bound' got status unknown.
-[eva:alarm] tests/arith/quantif.i:90: Warning:
+[eva:alarm] tests/arith/quantif.i:96: Warning:
assertion 'failded_missing_upper_bound' got status unknown.
-[eva:alarm] tests/arith/quantif.i:92: Warning:
+[eva:alarm] tests/arith/quantif.i:98: Warning:
assertion 'failed_invalid_upper_bound_1' got status unknown.
-[eva:alarm] tests/arith/quantif.i:94: Warning:
+[eva:alarm] tests/arith/quantif.i:100: Warning:
assertion 'failed_invalid_upper_bound_2' got status unknown.
-[eva:alarm] tests/arith/quantif.i:98: Warning:
+[eva:alarm] tests/arith/quantif.i:104: Warning:
assertion 'failed_multiple_upper_bounds' got status unknown.
-[eva:alarm] tests/arith/quantif.i:100: Warning:
+[eva:alarm] tests/arith/quantif.i:106: Warning:
assertion 'multiple_linked_upper' got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/quantif.i b/src/plugins/e-acsl/tests/arith/quantif.i
index c98110962b0f47441c9883ffa6c5d90249de46fd..01e7d23222887f27f5359a7bbdb93ce6f7ad0fbb 100644
--- a/src/plugins/e-acsl/tests/arith/quantif.i
+++ b/src/plugins/e-acsl/tests/arith/quantif.i
@@ -31,6 +31,12 @@ int main(void) {
/*@ assert \forall int x; 0 <= x < 10
==> x % 2 == 0 ==> \exists integer y; 0 <= y <= x/2 && x == 2 * y; */
+ // quantifications inside quantifications
+
+ /*@ assert \forall int x; 0 <= x < 10
+ ==> (\forall int y; 10 <= y < 20 ==> x <= y) &&
+ (\forall int y; -10 <= y < 0 ==> y <= x); */
+
{ // Gitlab issue #42
int buf[10];
unsigned long len = 9;