Skip to content
Snippets Groups Projects
Unverified Commit d4f6781b authored by Thibaut Benjamin's avatar Thibaut Benjamin
Browse files

[e-acsl] test for nested quantifiers

parent 52ea4b68
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+ 168
− 106
View file @ d4f6781b
......@@ -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;
}
src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
+ 27
− 27
View file @ d4f6781b
[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.
src/plugins/e-acsl/tests/arith/quantif.i
+ 6
− 0
View file @ d4f6781b
......@@ -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;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment