diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix
index 4b99a89ceca490cf47203fd76143a79885ff10a2..3ca82c80b2459cccb879668862953a4fc013ebbb 100644
--- a/nix/kernel-tests.nix
+++ b/nix/kernel-tests.nix
@@ -14,6 +14,7 @@ mk_tests {
       @tests/saveload/ptests \
       @tests/spec/ptests \
       @tests/syntax/ptests \
-      @tests/test/ptests
+      @tests/test/ptests \
+      @src/kernel_internals/parsing/tests/ptests
   '';
 }
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index fb91e86165755fdfcf0c4503b84707e95f82e9ca..d2bd2fcccbcae31952a79d589dc4303084a66559 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1145,7 +1145,13 @@ contract:
 // use that to detect potentially missing ';' at end of clause
 clause_kw:
 | ADMIT_REQUIRES { "admit requires" }
+| ADMIT_INVARIANT { "admit invariant" }
+| ADMIT_LEMMA { "admit lemma" }
+| ADMIT_LOOP { "admit loop" }
 | CHECK_REQUIRES { "check requires" }
+| CHECK_INVARIANT { "check invariant" }
+| CHECK_LEMMA { "check lemma" }
+| CHECK_LOOP { "check loop" }
 | REQUIRES { "requires" }
 | ASSUMES {"assumes"}
 | ASSIGNS { "assigns" }
@@ -1495,6 +1501,8 @@ beg_pragma_or_code_annotation:
 | INVARIANT {}
 | CHECK_INVARIANT {}
 | ADMIT_INVARIANT {}
+| CHECK_LOOP {}
+| ADMIT_LOOP {}
 | EXT_CODE_ANNOT {}
 ;
 
@@ -1871,7 +1879,7 @@ identifier_or_typename: /* allowed as C field names */
 | is_acsl_typename  { $1 }
 | TYPENAME { $1 } /* followed by the same list than 'identifier' */
 | IDENTIFIER { $1 }
-/* token list used inside ascl clauses: */
+/* token list used inside acsl clauses: */
 | BEHAVIORS  { "behaviors" }
 | LABEL      { "label" }
 | READS      { "reads" }
@@ -1880,7 +1888,7 @@ identifier_or_typename: /* allowed as C field names */
 
 identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
 | IDENTIFIER { $1 }
-/* token list used inside ascl clauses: */
+/* token list used inside acsl clauses: */
 | BEHAVIORS  { "behaviors" }
 | LABEL      { "label" }
 | READS      { "reads" }
@@ -1975,8 +1983,14 @@ is_acsl_decl_or_code_annot:
 | IMPACT    { "impact" }
 | INDUCTIVE { "inductive" }
 | INVARIANT { "invariant" }
+| ADMIT_INVARIANT { "admit invariant" }
+| CHECK_INVARIANT { "check invariant" }
 | LEMMA     { "lemma" }
+| ADMIT_LEMMA { "admit lemma" }
+| CHECK_LEMMA { "check lemma" }
 | LOOP      { "loop" }
+| ADMIT_LOOP { "admit loop" }
+| CHECK_LOOP { "check loop" }
 | PRAGMA    { "pragma" }
 | PREDICATE { "predicate" }
 | SLICE     { "slice" }
diff --git a/src/kernel_internals/parsing/tests/check_logic_parser.ml b/src/kernel_internals/parsing/tests/check_logic_parser.ml
index 38280b55d07b831d7dfdc3c5864bd4baee1c88f5..a61fac7f1b69d61059037280326980b7b1ef8614 100644
--- a/src/kernel_internals/parsing/tests/check_logic_parser.ml
+++ b/src/kernel_internals/parsing/tests/check_logic_parser.ml
@@ -28,7 +28,30 @@ let tokens = ref Strings.empty
 
 let wildcards = ref Strings.empty
 
-type state = Throw | Wildcard
+type state = Throw | Wildcard | Comment
+
+let remove_comment in_comm s =
+  let b = Buffer.create 5 in
+  let token (in_comm, prev) c =
+    if in_comm then begin
+      match prev, c with
+      | Some '*', '/' -> false, None
+      | _ -> true, Some c
+    end else begin
+      match prev, c with
+      | Some '/', '*' -> true, None
+      | Some c1, c2 ->
+        Buffer.add_char b c1; false, Some c2
+      | _ -> false, Some c
+    end
+  in
+  let (in_comm, last) = Seq.fold_left token (in_comm, None) (String.to_seq s) in
+  if not in_comm then begin
+    match last with
+    | Some c -> Buffer.add_char b c
+    | None -> ()
+  end;
+  in_comm, Buffer.contents b
 
 let is_token_line s = String.length s >= 6 && String.sub s 0 6 = "%token"
 
@@ -52,6 +75,7 @@ let add_tokens s =
 let wildcard_rules =
   [ "bs_keyword"; "wildcard"; "keyword"; "c_keyword";
     "non_logic_keyword"; "acsl_c_keyword"; "is_ext_spec";
+    "is_acsl_typename";
     "is_acsl_spec"; "is_acsl_decl_or_code_annot";
     "is_acsl_other"; "post_cond";
     "identifier_or_typename"
@@ -91,23 +115,41 @@ let add_wildcards s =
   if s <> "" then
     try
       add_wildcard s
-    with Scanf.Scan_failure _ -> ()
+    with Scanf.Scan_failure _ | End_of_file -> ()
 
 let () =
   try
-    let state = ref Throw in
+    let state = Stack.create () in
+    Stack.push Throw state;
     while true do
       let s = input_line file in
+      let in_comm, s = remove_comment (Stack.top state = Comment) s in
+      (* if we exit from comment, return to previous state and analyze line *)
+      if not in_comm && Stack.top state = Comment then begin
+        ignore (Stack.pop state);
+      end;
       if is_token_line s then add_tokens s
-      else if !state = Throw then begin
+      else if Stack.top state = Throw then begin
         if is_wildcard_rule s then begin
-          state:=Wildcard;
-          add_wildcards s
+          Stack.clear state;
+          Stack.push Wildcard state;
+          add_wildcards s;
+        end
+      end
+      else if Stack.top state = Wildcard then begin
+        if is_other_rule s then begin
+          Stack.clear state;
+          Stack.push Throw state;
         end
+        else begin
+          add_wildcards s;
+        end;
+      end;
+      (* if we have started an unfinished comment,
+         pass in comment mode for the next line. *)
+      if in_comm && Stack.top state <> Comment then begin
+        Stack.push Comment state;
       end
-      else (* state is Wildcard *)
-      if is_other_rule s then state:=Throw
-      else add_wildcards s
     done
   with End_of_file -> ()