diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index a4b18ac20739034825c65368744722c99554305f..c45d0439131d37ea213d85f8ace3f15580456644 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -68,12 +68,12 @@ PLUGIN_CMO:= \
LogicUsage RefUsage \
Layout Region \
RegionAnnot RegionAccess RegionDump RegionAnalysis \
- cil2cfg normAtLabels wpPropId wpStrategy mcfg \
+ cil2cfg normAtLabels wpPropId wpStrategy \
Lang Repr Matrix Passive Splitter \
LogicBuiltins Definitions \
Cmath Cint Cfloat Vset Vlist Cstring Cvalues \
Letify Cleaning \
- Sigs Mstate Conditions \
+ Mstate Conditions \
Filtering \
Plang Pcfg Pcond \
CodeSemantics \
@@ -103,7 +103,8 @@ PLUGIN_CMO:= \
wpGenerator cfgGenerator \
Generator register VC
-PLUGIN_CMI:=
+PLUGIN_CMI:= \
+ Sigs mcfg
PLUGIN_GENERATED:= \
$(PLUGIN_DIR)/script.ml \
@@ -237,12 +238,12 @@ WP_API_BASE= \
MemoryContext.mli \
LogicUsage.mli RefUsage.mli \
normAtLabels.mli \
- wpPropId.mli mcfg.ml \
+ wpPropId.mli mcfg.mli \
Context.mli Warning.mli AssignsCompleteness.mli wpContext.mli \
Lang.mli Repr.mli Passive.mli Splitter.mli \
LogicBuiltins.mli Definitions.mli \
Cint.mli Cfloat.mli Vset.mli Cstring.mli \
- Sigs.ml Mstate.mli Conditions.mli Filtering.mli \
+ Sigs.mli Mstate.mli Conditions.mli Filtering.mli \
Plang.mli Pcfg.mli Pcond.mli \
CodeSemantics.mli \
LogicCompiler.mli LogicSemantics.mli \
@@ -323,7 +324,7 @@ clean::
rm -f $(Wp_DIR)/share/install.cm*
$(Wp_DIR)/share/instwp: $(Wp_DIR)/share/install.ml
- $(OCAMLC) $(WARNINGS) -o $@ unix.cma $^
+ $(OCAMLC) $(WARNINGS) -w -70 -o $@ unix.cma $^
# --------------------------------------------------------------------------
# --- Pre-Compiled Coq Libraries ---
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.mli
similarity index 100%
rename from src/plugins/wp/Sigs.ml
rename to src/plugins/wp/Sigs.mli
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.mli
similarity index 100%
rename from src/plugins/wp/mcfg.ml
rename to src/plugins/wp/mcfg.mli
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index de651b862f8562d244218dabee2dba8dd3cb4a57..cd673ad5553ef608a18959dc17135fe8626d4443 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -22,30 +22,11 @@
let dkey_main = Wp_parameters.register_category "main"
let dkey_raised = Wp_parameters.register_category "raised"
-let wkey_smoke = Wp_parameters.register_warn_category "smoke"
(* ------------------------------------------------------------------------ *)
(* --- Memory Model Hypotheses --- *)
(* ------------------------------------------------------------------------ *)
-module Models = Set.Make(WpContext.MODEL)
-module Fmap = Kernel_function.Map
-
-let wp_iter_model ?ip ?index job =
- begin
- let pool : Models.t Fmap.t ref = ref Fmap.empty in
- Wpo.iter ?ip ?index ~on_goal:(fun wpo ->
- match Wpo.get_index wpo with
- | Wpo.Axiomatic _ -> ()
- | Wpo.Function(kf,_) ->
- let m = Wpo.get_model wpo in
- let ms = try Fmap.find kf !pool with Not_found -> Models.empty in
- if not (Models.mem m ms) then
- pool := Fmap.add kf (Models.add m ms) !pool ;
- ) () ;
- Fmap.iter (fun kf ms -> Models.iter (fun m -> job kf m) ms) !pool
- end
-
let wp_compute_memory_context model =
let hypotheses_computer = WpContext.compute_hypotheses model in
let name = WpContext.MODEL.id model in
@@ -136,12 +117,6 @@ let pp_warnings fmt wpo =
| false , _ -> Format.fprintf fmt " (Stronger, %d warnings)" n
end
-let launch task =
- let server = ProverTask.server () in
- (** Do on_server_stop save why3 session *)
- Task.spawn server (Task.thread task) ;
- Task.launch server
-
(* ------------------------------------------------------------------------ *)
(* --- Prover Stats --- *)
(* ------------------------------------------------------------------------ *)
@@ -755,21 +730,6 @@ let cmdline_run () =
end
end
-(* ------------------------------------------------------------------------ *)
-(* --- Register external functions --- *)
-(* ------------------------------------------------------------------------ *)
-
-let deprecated name =
- Wp_parameters.warning ~once:true ~current:false
- "Dynamic '%s' now is deprecated. Use `Wp.VC` api instead." name
-
-let register name ty code =
- let _ignore =
- Dynamic.register ~plugin:"Wp" name ty
- ~journalize:false (*LC: Because of Property is not journalizable. *)
- (fun x -> deprecated name ; code x)
- in ()
-
(* ------------------------------------------------------------------------ *)
(* --- Tracing WP Invocation --- *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/register.mli b/src/plugins/wp/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5ad2762fc1e77744ec9704c0ef2e23c0570206cc
--- /dev/null
+++ b/src/plugins/wp/register.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val do_wp_proofs:
+ ?provers:Why3.Whyconf.prover list -> ?tip:bool -> Wpo.t Bag.t -> unit