From 1b0b42c7e032b30a408d8bae152b2fd426ef8cb4 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 5 Sep 2024 13:43:53 +0200
Subject: [PATCH] [kernel] Register extensions in early stage
---
src/kernel_internals/typing/unfold_loops.ml | 8 +++++++-
src/kernel_services/ast_queries/dyncall.ml | 20 +++++++++-----------
2 files changed, 16 insertions(+), 12 deletions(-)
diff --git a/src/kernel_internals/typing/unfold_loops.ml b/src/kernel_internals/typing/unfold_loops.ml
index 73a2552df72..04d0a147953 100644
--- a/src/kernel_internals/typing/unfold_loops.ml
+++ b/src/kernel_internals/typing/unfold_loops.ml
@@ -757,5 +757,11 @@ let unroll_typer (ctxt: Logic_typing.typing_context) (_loc:location) args =
Lenv.empty () |> append_here_label |> append_init_label |> append_pre_label
in Ext_terms (List.map (ctxt.type_term ctxt env) args)
-let () = Acsl_extension.register_code_annot_next_loop
+let register_extensions () =
+ Acsl_extension.register_code_annot_next_loop
~plugin:"kernel" "unfold" unroll_typer false
+
+let register_once, _ =
+ State_builder.apply_once "Unfold_loops.register_extensions" [] register_extensions
+
+let () = Cmdline.run_after_early_stage register_once
diff --git a/src/kernel_services/ast_queries/dyncall.ml b/src/kernel_services/ast_queries/dyncall.ml
index 33c4789286e..15a73179dc9 100644
--- a/src/kernel_services/ast_queries/dyncall.ml
+++ b/src/kernel_services/ast_queries/dyncall.ml
@@ -250,15 +250,13 @@ let get ?bhv stmt =
(* --- Registry --- *)
(* -------------------------------------------------------------------------- *)
-let register =
- let once = ref false in
- fun () ->
- if (not !once) then begin
- once := true;
- Acsl_extension.register_code_annot_next_stmt ~plugin:"kernel"
- "calls" typecheck true ;
- Acsl_extension.register_behavior ~plugin:"kernel"
- "instanceof" typecheck true ;
- end
+let register_extensions () =
+ Acsl_extension.register_code_annot_next_stmt ~plugin:"kernel"
+ "calls" typecheck true;
+ Acsl_extension.register_behavior ~plugin:"kernel"
+ "instanceof" typecheck true
+
+let register_once, _ =
+ State_builder.apply_once "Dyncall.register_extensions" [] register_extensions
-let () = Cmdline.run_after_configuring_stage register
+let () = Cmdline.run_after_early_stage register_once
--
GitLab