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

[e-acsl] add quantification over enum types

parent d4889a53
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/src/analyses/typing.ml
+ 2
− 1
View file @ ca3715f7
......@@ -751,7 +751,8 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
| Linteger -> mk_ctx ~use_gmp_opt:true (ty_of_interv ~ctx:Gmpz i)
| Ctype ty ->
(match Cil.unrollType ty with
| TInt(ik, _) -> mk_ctx ~use_gmp_opt:true (C_integer ik)
| TInt(ik, _) | TEnum({ ekind = ik }, _) ->
mk_ctx ~use_gmp_opt:true (C_integer ik)
| ty ->
Options.fatal "unexpected C type %a for quantified variable %a"
Printer.pp_typ ty
......
src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+ 62
− 23
View file @ ca3715f7
......@@ -8,6 +8,10 @@
#include "time.h"
extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
enum RIGHT {
CREATE = 0,
DELETE = 1
};
/*@
predicate p1(integer i, integer j, integer k) =
0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12;
......@@ -64,7 +68,7 @@ int main(void)
__gen_e_acsl_assert_data.pred_txt = "\\forall integer x; 0 <= x <= 1 ==> x == 0 || x == 1";
__gen_e_acsl_assert_data.file = "quantif.i";
__gen_e_acsl_assert_data.fct = "main";
__gen_e_acsl_assert_data.line = 16;
__gen_e_acsl_assert_data.line = 17;
__e_acsl_assert(__gen_e_acsl_forall,& __gen_e_acsl_assert_data);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data);
}
......@@ -94,7 +98,7 @@ int main(void)
__gen_e_acsl_assert_data_2.pred_txt = "\\forall integer x; 0 < x <= 1 ==> x == 1";
__gen_e_acsl_assert_data_2.file = "quantif.i";
__gen_e_acsl_assert_data_2.fct = "main";
__gen_e_acsl_assert_data_2.line = 17;
__gen_e_acsl_assert_data_2.line = 18;
__e_acsl_assert(__gen_e_acsl_forall_2,& __gen_e_acsl_assert_data_2);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_2);
}
......@@ -124,7 +128,7 @@ int main(void)
__gen_e_acsl_assert_data_3.pred_txt = "\\forall integer x; 0 <= x < 1 ==> x == 0";
__gen_e_acsl_assert_data_3.file = "quantif.i";
__gen_e_acsl_assert_data_3.fct = "main";
__gen_e_acsl_assert_data_3.line = 18;
__gen_e_acsl_assert_data_3.line = 19;
__e_acsl_assert(__gen_e_acsl_forall_3,& __gen_e_acsl_assert_data_3);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_3);
}
......@@ -167,7 +171,7 @@ int main(void)
__gen_e_acsl_assert_data_4.pred_txt = "\\forall integer x, integer y, integer z;\n 0 <= x < 2 && 0 <= y < 5 && 0 <= z <= y ==> x + z <= y + 1";
__gen_e_acsl_assert_data_4.file = "quantif.i";
__gen_e_acsl_assert_data_4.fct = "main";
__gen_e_acsl_assert_data_4.line = 22;
__gen_e_acsl_assert_data_4.line = 23;
__e_acsl_assert(__gen_e_acsl_forall_4,& __gen_e_acsl_assert_data_4);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_4);
}
......@@ -202,7 +206,7 @@ int main(void)
__gen_e_acsl_assert_data_5.pred_txt = "\\exists int x; 0 <= x < 10 && x == 5";
__gen_e_acsl_assert_data_5.file = "quantif.i";
__gen_e_acsl_assert_data_5.fct = "main";
__gen_e_acsl_assert_data_5.line = 27;
__gen_e_acsl_assert_data_5.line = 28;
__e_acsl_assert(__gen_e_acsl_exists,& __gen_e_acsl_assert_data_5);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_5);
}
......@@ -253,7 +257,7 @@ int main(void)
__gen_e_acsl_assert_data_6.pred_txt = "\\forall int x;\n 0 <= x < 10 ==>\n x % 2 == 0 ==> (\\exists integer y; 0 <= y <= x / 2 && x == 2 * y)";
__gen_e_acsl_assert_data_6.file = "quantif.i";
__gen_e_acsl_assert_data_6.fct = "main";
__gen_e_acsl_assert_data_6.line = 31;
__gen_e_acsl_assert_data_6.line = 32;
__e_acsl_assert(__gen_e_acsl_forall_5,& __gen_e_acsl_assert_data_6);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_6);
}
......@@ -324,7 +328,7 @@ int main(void)
__gen_e_acsl_assert_data_7.pred_txt = "\\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)";
__gen_e_acsl_assert_data_7.file = "quantif.i";
__gen_e_acsl_assert_data_7.fct = "main";
__gen_e_acsl_assert_data_7.line = 36;
__gen_e_acsl_assert_data_7.line = 37;
__e_acsl_assert(__gen_e_acsl_forall_6,& __gen_e_acsl_assert_data_7);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_7);
}
......@@ -371,7 +375,7 @@ int main(void)
__gen_e_acsl_assert_data_8.pred_txt = "\\forall integer i; 0 <= i < 10 ==> \\valid(&buf[i])";
__gen_e_acsl_assert_data_8.file = "quantif.i";
__gen_e_acsl_assert_data_8.fct = "main";
__gen_e_acsl_assert_data_8.line = 43;
__gen_e_acsl_assert_data_8.line = 44;
__e_acsl_assert(__gen_e_acsl_forall_9,& __gen_e_acsl_assert_data_8);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_8);
}
......@@ -407,7 +411,7 @@ int main(void)
__gen_e_acsl_assert_data_9.pred_txt = "\\forall char i; 0 <= i < 10 ==> \\valid(&buf[i])";
__gen_e_acsl_assert_data_9.file = "quantif.i";
__gen_e_acsl_assert_data_9.fct = "main";
__gen_e_acsl_assert_data_9.line = 44;
__gen_e_acsl_assert_data_9.line = 45;
__e_acsl_assert(__gen_e_acsl_forall_10,& __gen_e_acsl_assert_data_9);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_9);
}
......@@ -443,7 +447,7 @@ int main(void)
__gen_e_acsl_assert_data_10.pred_txt = "\\forall integer i; 0 <= i < len ==> \\valid(&buf[i])";
__gen_e_acsl_assert_data_10.file = "quantif.i";
__gen_e_acsl_assert_data_10.fct = "main";
__gen_e_acsl_assert_data_10.line = 45;
__gen_e_acsl_assert_data_10.line = 46;
__e_acsl_assert(__gen_e_acsl_forall_11,& __gen_e_acsl_assert_data_10);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_10);
}
......@@ -508,7 +512,7 @@ int main(void)
__gen_e_acsl_assert_data_11.pred_txt = "\\forall integer i; 0 <= i <= len ==> \\valid(&buf[i])";
__gen_e_acsl_assert_data_11.file = "quantif.i";
__gen_e_acsl_assert_data_11.fct = "main";
__gen_e_acsl_assert_data_11.line = 46;
__gen_e_acsl_assert_data_11.line = 47;
__e_acsl_assert(__gen_e_acsl_forall_12,& __gen_e_acsl_assert_data_11);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_11);
__gmpz_clear(__gen_e_acsl_i_4);
......@@ -524,7 +528,7 @@ int main(void)
__gen_e_acsl_assert_data_12.pred_txt = "\\forall integer x; 0 < x < 1 ==> \\false";
__gen_e_acsl_assert_data_12.file = "quantif.i";
__gen_e_acsl_assert_data_12.fct = "main";
__gen_e_acsl_assert_data_12.line = 50;
__gen_e_acsl_assert_data_12.line = 51;
__e_acsl_assert(1,& __gen_e_acsl_assert_data_12);
}
/*@ assert \forall integer x; 0 < x < 1 ==> \false; */ ;
......@@ -536,7 +540,7 @@ int main(void)
__gen_e_acsl_assert_data_13.pred_txt = "!(\\exists char c; 10 <= c < 10 && c == 10)";
__gen_e_acsl_assert_data_13.file = "quantif.i";
__gen_e_acsl_assert_data_13.fct = "main";
__gen_e_acsl_assert_data_13.line = 51;
__gen_e_acsl_assert_data_13.line = 52;
__e_acsl_assert(1,& __gen_e_acsl_assert_data_13);
}
/*@ assert !(\exists char c; 10 <= c < 10 && c == 10); */ ;
......@@ -550,7 +554,7 @@ int main(void)
__gen_e_acsl_assert_data_14.pred_txt = "\\let u = 5;\n\\forall integer x, integer y; 0 <= x < 2 && 4 < y < u ==> \\false";
__gen_e_acsl_assert_data_14.file = "quantif.i";
__gen_e_acsl_assert_data_14.fct = "main";
__gen_e_acsl_assert_data_14.line = 53;
__gen_e_acsl_assert_data_14.line = 54;
__e_acsl_assert(1,& __gen_e_acsl_assert_data_14);
}
/*@
......@@ -600,7 +604,7 @@ int main(void)
__gen_e_acsl_assert_data_15.pred_txt = "\\forall integer i, integer j, integer k;\n 0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12 ==> p1(i, j, k)";
__gen_e_acsl_assert_data_15.file = "quantif.i";
__gen_e_acsl_assert_data_15.fct = "main";
__gen_e_acsl_assert_data_15.line = 59;
__gen_e_acsl_assert_data_15.line = 60;
__gen_e_acsl_assert_data_15.name = "forall_multiple_binders_1";
__e_acsl_assert(__gen_e_acsl_forall_13,& __gen_e_acsl_assert_data_15);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_15);
......@@ -655,7 +659,7 @@ int main(void)
__gen_e_acsl_assert_data_16.pred_txt = "\\forall integer i, integer j, integer k;\n 0 <= i <= j < k <= 10 ==> p2(i, j, k)";
__gen_e_acsl_assert_data_16.file = "quantif.i";
__gen_e_acsl_assert_data_16.fct = "main";
__gen_e_acsl_assert_data_16.line = 62;
__gen_e_acsl_assert_data_16.line = 63;
__gen_e_acsl_assert_data_16.name = "forall_multiple_binders_2";
__e_acsl_assert(__gen_e_acsl_forall_14,& __gen_e_acsl_assert_data_16);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_16);
......@@ -710,7 +714,7 @@ int main(void)
__gen_e_acsl_assert_data_17.pred_txt = "\\forall integer i, integer j, integer k;\n 0 <= i < j <= 10 && 1 < k < 11 ==> p3(i, j, k)";
__gen_e_acsl_assert_data_17.file = "quantif.i";
__gen_e_acsl_assert_data_17.fct = "main";
__gen_e_acsl_assert_data_17.line = 65;
__gen_e_acsl_assert_data_17.line = 66;
__gen_e_acsl_assert_data_17.name = "forall_multiple_binders_3";
__e_acsl_assert(__gen_e_acsl_forall_15,& __gen_e_acsl_assert_data_17);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_17);
......@@ -765,7 +769,7 @@ int main(void)
__gen_e_acsl_assert_data_18.pred_txt = "\\forall integer i, integer j, integer k;\n 0 <= i < 10 ==> 1 < j <= 11 ==> 2 <= k <= 12 ==> p1(i, j, k)";
__gen_e_acsl_assert_data_18.file = "quantif.i";
__gen_e_acsl_assert_data_18.fct = "main";
__gen_e_acsl_assert_data_18.line = 68;
__gen_e_acsl_assert_data_18.line = 69;
__gen_e_acsl_assert_data_18.name = "forall_multiple_binders_4";
__e_acsl_assert(__gen_e_acsl_forall_16,& __gen_e_acsl_assert_data_18);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_18);
......@@ -820,7 +824,7 @@ int main(void)
__gen_e_acsl_assert_data_19.pred_txt = "\\forall integer i, integer j, integer k;\n 0 <= i <= k <= 10 && 1 <= j < k ==> p4(i, j, k)";
__gen_e_acsl_assert_data_19.file = "quantif.i";
__gen_e_acsl_assert_data_19.fct = "main";
__gen_e_acsl_assert_data_19.line = 71;
__gen_e_acsl_assert_data_19.line = 72;
__gen_e_acsl_assert_data_19.name = "forall_unordered_binders";
__e_acsl_assert(__gen_e_acsl_forall_17,& __gen_e_acsl_assert_data_19);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_19);
......@@ -875,7 +879,7 @@ int main(void)
__gen_e_acsl_assert_data_20.pred_txt = "\\exists integer i, integer j, integer k;\n 0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12 && p1(i, j, k)";
__gen_e_acsl_assert_data_20.file = "quantif.i";
__gen_e_acsl_assert_data_20.fct = "main";
__gen_e_acsl_assert_data_20.line = 74;
__gen_e_acsl_assert_data_20.line = 75;
__gen_e_acsl_assert_data_20.name = "exists_multiple_binders_1";
__e_acsl_assert(__gen_e_acsl_exists_3,& __gen_e_acsl_assert_data_20);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_20);
......@@ -930,7 +934,7 @@ int main(void)
__gen_e_acsl_assert_data_21.pred_txt = "\\exists integer i, integer j, integer k; 0 <= i <= j < k <= 10 && p2(i, j, k)";
__gen_e_acsl_assert_data_21.file = "quantif.i";
__gen_e_acsl_assert_data_21.fct = "main";
__gen_e_acsl_assert_data_21.line = 77;
__gen_e_acsl_assert_data_21.line = 78;
__gen_e_acsl_assert_data_21.name = "exists_multiple_binders_2";
__e_acsl_assert(__gen_e_acsl_exists_4,& __gen_e_acsl_assert_data_21);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_21);
......@@ -985,7 +989,7 @@ int main(void)
__gen_e_acsl_assert_data_22.pred_txt = "\\exists integer i, integer j, integer k;\n 0 <= i < j <= 10 && 1 < k < 11 && p3(i, j, k)";
__gen_e_acsl_assert_data_22.file = "quantif.i";
__gen_e_acsl_assert_data_22.fct = "main";
__gen_e_acsl_assert_data_22.line = 80;
__gen_e_acsl_assert_data_22.line = 81;
__gen_e_acsl_assert_data_22.name = "exists_multiple_binders_3";
__e_acsl_assert(__gen_e_acsl_exists_5,& __gen_e_acsl_assert_data_22);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_22);
......@@ -1040,7 +1044,7 @@ int main(void)
__gen_e_acsl_assert_data_23.pred_txt = "\\exists integer i, integer j, integer k;\n 0 <= i <= k <= 10 && 1 <= j < k && p4(i, j, k)";
__gen_e_acsl_assert_data_23.file = "quantif.i";
__gen_e_acsl_assert_data_23.fct = "main";
__gen_e_acsl_assert_data_23.line = 83;
__gen_e_acsl_assert_data_23.line = 84;
__gen_e_acsl_assert_data_23.name = "exists_unordered_binders";
__e_acsl_assert(__gen_e_acsl_exists_6,& __gen_e_acsl_assert_data_23);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_23);
......@@ -1115,6 +1119,41 @@ int main(void)
0 <= i < 10 && 2 <= i < 8 && 4 <= j < 6 ==> p1(i, j, 2);
*/
;
{
int __gen_e_acsl_forall_18;
int __gen_e_acsl_r;
__e_acsl_assert_data_t __gen_e_acsl_assert_data_35 =
{.values = (void *)0};
__gen_e_acsl_forall_18 = 1;
__gen_e_acsl_r = 0U;
while (1) {
if (__gen_e_acsl_r < 1) ; else break;
{
int __gen_e_acsl_and_18;
if (1 <= __gen_e_acsl_r + 1) __gen_e_acsl_and_18 = __gen_e_acsl_r + 1 < 2;
else __gen_e_acsl_and_18 = 0;
if (__gen_e_acsl_and_18) ;
else {
__gen_e_acsl_forall_18 = 0;
goto e_acsl_end_loop24;
}
}
__gen_e_acsl_r ++;
}
e_acsl_end_loop24: ;
__e_acsl_assert_register_int(& __gen_e_acsl_assert_data_35,
"\\forall enum RIGHT r; 0 <= r < 1 ==> 1 <= r + 1 < 2",
0,__gen_e_acsl_forall_18);
__gen_e_acsl_assert_data_35.blocking = 1;
__gen_e_acsl_assert_data_35.kind = "Assertion";
__gen_e_acsl_assert_data_35.pred_txt = "\\forall enum RIGHT r; 0 <= r < 1 ==> 1 <= r + 1 < 2";
__gen_e_acsl_assert_data_35.file = "quantif.i";
__gen_e_acsl_assert_data_35.fct = "main";
__gen_e_acsl_assert_data_35.line = 112;
__e_acsl_assert(__gen_e_acsl_forall_18,& __gen_e_acsl_assert_data_35);
__e_acsl_assert_clean(& __gen_e_acsl_assert_data_35);
}
/*@ assert \forall enum RIGHT r; 0 <= r < 1 ==> 1 <= r + 1 < 2; */ ;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
......
src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
+ 29
− 29
View file @ ca3715f7
[e-acsl] beginning translation.
[e-acsl] quantif.i:88: Warning:
[e-acsl] quantif.i:89: Warning:
invalid E-ACSL construct
`invalid guard 10 > i in quantification
failed_invalid_guards: \forall integer i; 10 > i >= 0 ==> p1(i, 2, 2).
Missing guard for i. Only < and <= are allowed to guard quantifier variables'.
Ignoring annotation.
[e-acsl] quantif.i:90: Warning:
[e-acsl] quantif.i:91: Warning:
invalid E-ACSL construct
`invalid guard p1(i, j, k) in quantification
failed_unguarded_k:
......@@ -13,58 +13,58 @@
0 <= i < 10 && 1 < j <= 11 ==> p1(i, j, k).
Missing guard for k. '.
Ignoring annotation.
[e-acsl] quantif.i:92: Warning:
[e-acsl] quantif.i:93: Warning:
E-ACSL construct
`non integer variable i in quantification
failed_non_integer: \forall real i; 0 <= i < 10 ==> p1(\truncate(i), 2, 2)'
is not yet supported.
Ignoring annotation.
[e-acsl] quantif.i:94: Warning:
[e-acsl] quantif.i:95: Warning:
invalid E-ACSL construct
`missing lower bound for i in quantification
failed_missing_lower_bound: \forall integer i; i < 10 ==> p1(i, 2, 2)'.
Ignoring annotation.
[e-acsl] quantif.i:96: Warning:
[e-acsl] quantif.i:97: Warning:
invalid E-ACSL construct
`invalid guard p1(i, 2, 2) in quantification
failded_missing_upper_bound: \forall integer i; 0 <= i ==> p1(i, 2, 2).
Missing upper bound for i. '.
Ignoring annotation.
[e-acsl] quantif.i:98: Warning:
[e-acsl] quantif.i:99: Warning:
invalid E-ACSL construct
`invalid guard p1(i, j, 2) in quantification
failed_invalid_upper_bound_1:
\forall integer i, integer j; 0 <= i < j ==> p1(i, j, 2).
Missing upper bound for j. '.
Ignoring annotation.
[e-acsl] quantif.i:100: Warning:
[e-acsl] quantif.i:101: 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:
\forall integer i, integer j; i < j && 0 <= i ==> p1(i, 2, 2)'.
Ignoring annotation.
[e-acsl] quantif.i:102: Warning:
[e-acsl] quantif.i:103: Warning:
invalid E-ACSL construct
`found existing lower bound i < j when processing 3 <= j in quantification
failed_extra_constraint:
\forall integer i, integer j;
0 <= i < j && i < 10 && 3 <= j < 5 ==> p1(i, j, 2)'.
Ignoring annotation.
[e-acsl] quantif.i:104: Warning:
[e-acsl] quantif.i:105: Warning:
invalid E-ACSL construct
`found existing lower bound 0 <= i when processing j < i in quantification
failed_multiple_upper_bounds:
\forall integer i, integer j; 0 <= i < j < i && j <= 10 ==> p1(i, j, 2)'.
Ignoring annotation.
[e-acsl] quantif.i:106: Warning:
[e-acsl] quantif.i:107: Warning:
invalid E-ACSL construct
`found existing lower bound i < k when processing j < k in quantification
multiple_linked_upper:
\forall integer i, integer j, integer k;
0 <= i < k && 1 <= j < k && 2 <= k < 10 ==> p1(i, j, k)'.
Ignoring annotation.
[e-acsl] quantif.i:108: Warning:
[e-acsl] quantif.i:109: Warning:
invalid E-ACSL construct
`invalid constraint 2 <= i, both operands are constants or already bounded in quantification
multiple_guard:
......@@ -72,36 +72,36 @@
0 <= i < 10 && 2 <= i < 8 && 4 <= j < 6 ==> p1(i, j, 2)'.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] quantif.i:22: Warning: assertion got status unknown.
[eva:alarm] quantif.i:31: Warning: assertion got status unknown.
[eva:alarm] quantif.i:46: Warning:
[eva:alarm] quantif.i:23: Warning: assertion got status unknown.
[eva:alarm] quantif.i:32: Warning: assertion got status unknown.
[eva:alarm] quantif.i:47: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] quantif.i:53: Warning: assertion got status unknown.
[eva:alarm] quantif.i:62: Warning:
[eva:alarm] quantif.i:54: Warning: assertion got status unknown.
[eva:alarm] quantif.i:63: Warning:
assertion 'forall_multiple_binders_2' got status unknown.
[eva:alarm] quantif.i:65: Warning:
[eva:alarm] quantif.i:66: Warning:
assertion 'forall_multiple_binders_3' got status unknown.
[eva:alarm] quantif.i:71: Warning:
[eva:alarm] quantif.i:72: Warning:
assertion 'forall_unordered_binders' got status unknown.
[eva:alarm] quantif.i:77: Warning:
[eva:alarm] quantif.i:78: Warning:
assertion 'exists_multiple_binders_2' got status unknown.
[eva:alarm] quantif.i:80: Warning:
[eva:alarm] quantif.i:81: Warning:
assertion 'exists_multiple_binders_3' got status unknown.
[eva:alarm] quantif.i:83: Warning:
[eva:alarm] quantif.i:84: Warning:
assertion 'exists_unordered_binders' got status unknown.
[eva:alarm] quantif.i:90: Warning:
[eva:alarm] quantif.i:91: Warning:
assertion 'failed_unguarded_k' got status unknown.
[eva:alarm] quantif.i:92: Warning:
[eva:alarm] quantif.i:93: Warning:
assertion 'failed_non_integer' got status unknown.
[eva:alarm] quantif.i:94: Warning:
[eva:alarm] quantif.i:95: Warning:
assertion 'failed_missing_lower_bound' got status unknown.
[eva:alarm] quantif.i:96: Warning:
[eva:alarm] quantif.i:97: Warning:
assertion 'failded_missing_upper_bound' got status unknown.
[eva:alarm] quantif.i:98: Warning:
[eva:alarm] quantif.i:99: Warning:
assertion 'failed_invalid_upper_bound_1' got status unknown.
[eva:alarm] quantif.i:100: Warning:
[eva:alarm] quantif.i:101: Warning:
assertion 'failed_invalid_upper_bound_2' got status unknown.
[eva:alarm] quantif.i:104: Warning:
[eva:alarm] quantif.i:105: Warning:
assertion 'failed_multiple_upper_bounds' got status unknown.
[eva:alarm] quantif.i:106: Warning:
[eva:alarm] quantif.i:107: Warning:
assertion 'multiple_linked_upper' got status unknown.
src/plugins/e-acsl/tests/arith/quantif.i
+ 4
− 0
View file @ ca3715f7
......@@ -2,6 +2,7 @@
COMMENT: quantifiers
STDOPT: +"-eva-min-loop-unroll=15"
*/
typedef enum RIGHT { CREATE, DELETE } right;
// Support predicates for some tests
//@ predicate p1(integer i, integer j, integer k) = 0 <= i < 10 && 1 < j <= 11 && 2 <= k <= 12;
......@@ -107,5 +108,8 @@ int main(void) {
/*@ assert multiple_guard:
\forall integer i,j; 0 <= i < 10 && 2 <= i < 8 && 4 <= j < 6 ==> p1(i,j,2); */
// Gitlab issue e-acsl#199
/*@ assert \forall right r; 0 <= r < 1 ==> 1 <= r+1 < 2; */
return 0;
}
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