[logic] allow empty list of arguments after an extension keyword.

src/kernel_internals/parsing/logic_parser.mly

@@ -1189,14 +1189,23 @@ ne_simple_clauses:
 | post_cond_kind full_lexpr clause_kw { missing 2 ";" $3 }
 | allocation clause_kw { missing 1 ";" $2 }
 | ASSIGNS full_assigns clause_kw { missing 2 ";" $3 }
-| EXT_CONTRACT grammar_extension clause_kw { missing 1 ";" $3 }
+| EXT_CONTRACT ne_grammar_extension clause_kw { missing 1 ";" $3 }
 ;
 
-grammar_extension:
-/* Grammar Extensibility for plugins */
+ne_grammar_extension:
 | full_zones { $1 }
 ;
 
+/* possibly empty list of terms, for ACSL extensions registered by plugins. */
+grammar_extension:
+| enter_kw_c_mode extension_content exit_kw_c_mode { $2 }
+;
+
+extension_content:
+| /* epsilon */ { [] }
+| zones { $1 }
+;
+
 post_cond_kind:
 | post_cond { fst $1 }
 ;

tests/spec/Extend.i

@@ -48,6 +48,7 @@ void loop (void) {
   //@ for ca_foo: ca_foo \true;
   //@ ns_foo \true;
   //@ baz \true;
+  //@ empty_extension;
   /*@ loop invariant \true; */
   while (0) { }
 }

tests/spec/Extend.ml

@@ -104,6 +104,10 @@ let type_bla typing_context _loc l =
   in
   Ext_preds l
 
+let type_empty _ loc = function
+  | [] -> Ext_terms [];
+  | _ -> Kernel.abort ~loc "empty_extension should not have arguments"
+
 let () =
   Acsl_extension.register_behavior "foo" type_foo false ;
   Acsl_extension.register_code_annot_next_loop "lfoo" type_foo false ;
@@ -113,7 +117,8 @@ let () =
   Acsl_extension.register_behavior
     "bar" type_bar ~printer:print_bar ~visitor:visit_bar false ;
   Acsl_extension.register_behavior "bla" type_bla false ;
-  Acsl_extension.register_code_annot_next_both "baz" type_baz false
+  Acsl_extension.register_code_annot_next_both "baz" type_baz false;
+  Acsl_extension.register_code_annot "empty_extension" type_empty false
 
 let run () =
   Ast.compute ();

tests/spec/oracle/Extend.res.oracle

@@ -55,6 +55,7 @@ void loop(void)
   /*@ for ca_foo: ca_foo \true; */ ;
   /*@ ns_foo \true; */
   /*@ baz \true; */
+  /*@ empty_extension ; */
   /*@ loop invariant \true; */
   while (1) break;
   return;