From d4f6781b4b39fab3f838c920959ad4dd36b28b65 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Mon, 2 Aug 2021 15:51:27 +0200
Subject: [PATCH] [e-acsl] test for nested quantifiers
---
.../e-acsl/tests/arith/oracle/gen_quantif.c | 274 +++++++++++-------
.../tests/arith/oracle/quantif.res.oracle | 54 ++--
src/plugins/e-acsl/tests/arith/quantif.i | 6 +
3 files changed, 201 insertions(+), 133 deletions(-)
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 ae624f3a5dd..bcf3490acf1 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -196,14 +196,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;
@@ -214,22 +276,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;
@@ -240,22 +302,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;
@@ -266,22 +328,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_;
@@ -309,8 +371,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;
}
}
{
@@ -327,10 +389,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]); */ ;
@@ -338,29 +400,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;
@@ -377,8 +439,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 ++;
@@ -387,10 +449,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
@@ -400,11 +462,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;
@@ -421,8 +483,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 ++;
@@ -431,10 +493,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
@@ -443,11 +505,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;
@@ -464,8 +526,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 ++;
@@ -474,10 +536,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
@@ -487,11 +549,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;
@@ -508,8 +570,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 ++;
@@ -518,10 +580,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
@@ -531,11 +593,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;
@@ -552,8 +614,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 ++;
@@ -562,10 +624,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
@@ -597,7 +659,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 ++;
@@ -606,10 +668,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
@@ -641,7 +703,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 ++;
@@ -650,10 +712,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
@@ -684,7 +746,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 ++;
@@ -693,10 +755,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
@@ -728,7 +790,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 ++;
@@ -737,10 +799,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
@@ -814,72 +876,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 b588f0c95ed..2eaa50601e5 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 c98110962b0..01e7d232228 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;
--
GitLab