From bdd9a03c011ce629207673af627df2c83e072c93 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Fri, 5 Jul 2024 12:03:19 +0200
Subject: [PATCH] [wp] Fixed top level importer registration

---
 src/plugins/wp/Why3Import.ml | 33 +++++++++++++++------------------
 1 file changed, 15 insertions(+), 18 deletions(-)

diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index d9d22eda7af..27c40582605 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -32,24 +32,6 @@ module WConf = Why3.Whyconf
 
 let dkey = L.register_category "why3.import"
 
-(* -------------------------------------------------------------------------- *)
-(* ---    Module registration                                             --- *)
-(* -------------------------------------------------------------------------- *)
-
-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
-    let k = Cil_const.make_logic_var_formal "k" Linteger in
-    check.l_profile <- [x;k] ;
-    ctxt.add_logic_type loc t ;
-    ctxt.add_logic_function loc check ;
-  end
-
-let () = Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader
-
 (* -------------------------------------------------------------------------- *)
 (* ---    Why3 Environment                                                --- *)
 (* -------------------------------------------------------------------------- *)
@@ -338,6 +320,21 @@ let import_theory (env : env) thname =
 (* ---    Module registration                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
+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
+    let k = Cil_const.make_logic_var_formal "k" Linteger in
+    check.l_profile <- [x;k] ;
+    ctxt.add_logic_type loc t ;
+    ctxt.add_logic_function loc check ;
+  end
+
+let () = Acsl_extension.register_module_importer ~plugin:"wp" "why3" loader
+
+
 (* -------------------------------------------------------------------------- *)
 (* ---    Main                                                            --- *)
 (* -------------------------------------------------------------------------- *)
-- 
GitLab