[kernel] support for parsing/printing check of generalized invariant

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
 }

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

tests/spec/generalized_check.i

 /* 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 : ;
+}

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;
+}
+