[wp] Registering module importer

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