From ca3715f7e39e7769c1a491e9003e0e247e75fa43 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@gmail.com>
Date: Mon, 23 May 2022 14:33:19 +0200
Subject: [PATCH] [e-acsl] add quantification over enum types
---
src/plugins/e-acsl/src/analyses/typing.ml | 3 +-
.../e-acsl/tests/arith/oracle/gen_quantif.c | 85 ++++++++++++++-----
.../tests/arith/oracle/quantif.res.oracle | 58 ++++++-------
src/plugins/e-acsl/tests/arith/quantif.i | 4 +
4 files changed, 97 insertions(+), 53 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index b83df3af03d..b3cb3df086f 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -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
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 6a2abd1e2af..9ac7afd8b8e 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
@@ -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;
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 5266a21d44a..975e9069daf 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
@@ -1,11 +1,11 @@
[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.
diff --git a/src/plugins/e-acsl/tests/arith/quantif.i b/src/plugins/e-acsl/tests/arith/quantif.i
index 01e7d232228..47edbd62c8f 100644
--- a/src/plugins/e-acsl/tests/arith/quantif.i
+++ b/src/plugins/e-acsl/tests/arith/quantif.i
@@ -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;
}
--
GitLab