diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 38d5b09db50efc5c67c3e204aa83669652d7c1a1..0bff4b69eda3bb3a77ca80cddbc3294ddbc2acfb 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/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 }
 ;
diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i
index ff81bb51cab62adebb757548a563b5c5c4ac1a00..85228eb7dfdf70924f95f5c26350fd051eff3b58 100644
--- a/tests/spec/Extend.i
+++ b/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) { }
 }
diff --git a/tests/spec/Extend.ml b/tests/spec/Extend.ml
index 99c5ea7064b6b8ad3de11702dafa936b3320e5e6..71fcdbdc871433955ef45aa232fd62b5f0c3b93b 100644
--- a/tests/spec/Extend.ml
+++ b/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 ();
diff --git a/tests/spec/oracle/Extend.res.oracle b/tests/spec/oracle/Extend.res.oracle
index 6fb85da86bac26486fff0df9fa0c8dfba1551d99..8bdcb407b189715c985896e27d32b22d5d209880 100644
--- a/tests/spec/oracle/Extend.res.oracle
+++ b/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;