From 0d2b237ba12b2eb64114f278c49527fd7c4fb1b8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 7 Sep 2020 17:04:44 +0200
Subject: [PATCH] [kernel] support for parsing/printing check of generalized
invariant
---
src/kernel_internals/parsing/logic_lexer.mll | 1 +
src/kernel_internals/parsing/logic_parser.mly | 5 ++++-
tests/spec/generalized_check.i | 13 +++++++++++-
.../spec/oracle/generalized_check.res.oracle | 20 +++++++++++++++++--
4 files changed, 35 insertions(+), 4 deletions(-)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 2441a0d268a..b86e9200489 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -306,6 +306,7 @@
| CHECK, BREAKS -> true, CHECK_BREAKS
| CHECK, CONTINUES -> true, CHECK_CONTINUES
| CHECK, LOOP -> true, CHECK_LOOP
+ | CHECK, INVARIANT -> true, CHECK_INVARIANT
| CHECK, LEMMA -> true, CHECK_LEMMA
| _ -> false, current
}
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index f2d84d9f7b4..38d5b09db50 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -251,7 +251,7 @@
%token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK SEMICOLON NULL EMPTY
%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
-%token CHECK_REQUIRES CHECK_LOOP CHECK_LEMMA
+%token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
@@ -1449,6 +1449,7 @@ beg_pragma_or_code_annotation:
| ASSERT {}
| CHECK {}
| INVARIANT {}
+| CHECK_INVARIANT {}
| EXT_CODE_ANNOT {}
;
@@ -1465,6 +1466,8 @@ code_annotation:
{ fun bhvs -> AAssert (bhvs,toplevel_pred true $2) }
| INVARIANT full_lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred false $2) }
+| CHECK_INVARIANT full_lexpr SEMICOLON
+ { fun bhvs -> AInvariant (bhvs,false,toplevel_pred true $2) }
| EXT_CODE_ANNOT grammar_extension SEMICOLON
{ fun bhvs ->
let open Cil_types in
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
index 06d4c500341..657ce7a76ab 100644
--- a/tests/spec/generalized_check.i
+++ b/tests/spec/generalized_check.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
+OPT: -wp-fct f,main -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
*/
/*@ check lemma easy_proof: \false; */ // should not be put in any environment
@@ -17,3 +17,14 @@ int main() {
f(&a);
/*@ check a == 0; */ // can't be proved by WP: we ignore the ensures
}
+
+void loop () {
+ /*@ check loop invariant \true; */
+ for (int i = 0; i< 10; i++);
+ int j = 0;
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j++;
+ goto l;
+ l1 : ;
+}
diff --git a/tests/spec/oracle/generalized_check.res.oracle b/tests/spec/oracle/generalized_check.res.oracle
index bb54dad662f..bcd2e1756d5 100644
--- a/tests/spec/oracle/generalized_check.res.oracle
+++ b/tests/spec/oracle/generalized_check.res.oracle
@@ -5,7 +5,7 @@
[wp:strategy] take f_assigns *x;
[wp:strategy] [add_node_annots] on <stmt-1>
[wp:strategy] [add_node_annots] on <stmt-2>
-[wp:strategy] [add_node_annots] on <stmt-10>
+[wp:strategy] [add_node_annots] on <stmt-30>
[wp:strategy] 'main' is the main entry point
[wp:strategy] [add_node_annots] on <stmt-5>
[wp:strategy] [add_node_annots] on <callIn-6>
@@ -13,7 +13,7 @@
[wp:strategy] [add_node_annots] on <callIn-6>
[wp:strategy] [add_node_annots] on <stmt-7>
[wp:strategy] [add_node_annots] on <stmt-8>
-[wp:strategy] [add_node_annots] on <stmt-12>
+[wp:strategy] [add_node_annots] on <stmt-32>
[wp] Warning: Missing RTE guards
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
@@ -125,4 +125,20 @@ int main(void)
return __retres;
}
+void loop(void)
+{
+ {
+ int i = 0;
+ /*@ check loop invariant \true; */
+ while (i < 10) i ++;
+ }
+ int j = 0;
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j ++;
+ goto l;
+ l1: ;
+ return;
+}
+
--
GitLab