From b338627c2e70af1ce836eb940d00a5794ce62439 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Fri, 5 Jul 2024 11:22:17 +0200
Subject: [PATCH] [wp] Registering module importer
---
src/plugins/wp/Why3Import.ml | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 45336714c7e..3217a7fc751 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -320,10 +320,9 @@ let import_theory (env : env) thname =
(* --- Module registration --- *)
(* -------------------------------------------------------------------------- *)
-(* let loader (ctxt: Logic_typing.module_builder) (loc: C.location) (m: string list) =
- begin
- Format.printf "[test-import:%d] Loading %s.@."
- (fst loc).pos_lnum (String.concat "::" m) ;
+let loader (ctxt: Logic_typing.module_builder) (loc: C.location) (m: string list) =
+ begin
+ L.result "[test-import:%d] Loading %s.@." (fst loc).pos_lnum (String.concat "::" m) ;
let t = Cil_const.make_logic_type "t" in
let check = Cil_const.make_logic_info "check" in
let x = Cil_const.make_logic_var_formal "x" (Ltype(t,[])) in
@@ -331,12 +330,12 @@ let import_theory (env : env) thname =
check.l_profile <- [x;k] ;
ctxt.add_logic_type loc t ;
ctxt.add_logic_function loc check ;
- end
+ end
- let register () =
- begin
- Acsl_extension.register_module_importer "Why3" loader
- end *)
+let register () =
+ begin
+ Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader
+ end
(* -------------------------------------------------------------------------- *)
@@ -346,6 +345,7 @@ let import_theory (env : env) thname =
let () =
Boot.Main.extend
begin fun () ->
+ register ();
let libs = L.Library.get() in
let imports = L.Import.get() in
if libs <> [] || imports <> [] then
--
GitLab