[wp] module why3-import

src/plugins/wp/Why3Import.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+module L = Wp_parameters
+
+(* -------------------------------------------------------------------------- *)
+
+let () =
+  Boot.Main.extend
+    begin fun () ->
+      let libs = L.Library.get () in
+      List.iter
+        (fun dir ->
+           L.debug ~level:1 " + LIB %a@." Filepath.Normalized.pretty dir
+        ) libs ;
+      let thys = L.Import.get () in
+      List.iter
+        (fun thy ->
+           L.debug ~level:1 " + THY %s@." thy
+        ) thys ;
+    end
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/Why3Import.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2023                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/wp_parameters.ml

@@ -839,6 +839,28 @@ module Tactics = String_list
     end)
 let () = on_reset Tactics.clear
 
+let () = Parameter_customize.set_group wp_prover
+let () = Parameter_customize.is_invisible ()
+module Import =
+  String_list
+    (struct
+      let option_name = "-wp-import"
+      let arg_name = "thy,..."
+      let help = "Import Why3 theories"
+    end)
+
+let () = Parameter_customize.set_group wp_prover
+let () = Parameter_customize.is_invisible ()
+module Library =
+  Filepath_list
+    (struct
+      let option_name = "-wp-library"
+      let arg_name = "dir,..."
+      let file_kind = "Why3 load path"
+      let existence = Fc_Filepath.Must_exist
+      let help = "Load path for importing why3 theories"
+    end)
+
 let () = Parameter_customize.set_group wp_prover
 module Drivers =
   Filepath_list

src/plugins/wp/wp_parameters.mli

@@ -126,6 +126,8 @@ module Cache: Parameter_sig.String
 module CacheEnv: Parameter_sig.Bool
 module CacheDir: Parameter_sig.String
 module CachePrint: Parameter_sig.Bool
+module Import: Parameter_sig.String_list
+module Library: Parameter_sig.Filepath_list
 module Drivers: Parameter_sig.Filepath_list
 module Timeout: Parameter_sig.Int
 module Memlimit: Parameter_sig.Int