diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 913d151300efeb21ff7da03a4f26e85693225926..e45f966ff83524b06b9706fab9436b7a648242e8 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -50,3 +50,5 @@ val parse :
Apply specifications to default setup.
Default setup is [Factory.default].
Default warning is [Wp_parameters.abort]. *)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml
index 07056383cae40e184e59c80043902c57f933423b..dbe1955809014faaf21086bcd0511374e55b5f31 100644
--- a/src/plugins/wp/Generator.ml
+++ b/src/plugins/wp/Generator.ml
@@ -20,9 +20,6 @@
(* *)
(**************************************************************************)
-open Cil_types
-open Wp_parameters
-
(* -------------------------------------------------------------------------- *)
(* --- Model Setup --- *)
(* -------------------------------------------------------------------------- *)
@@ -60,23 +57,11 @@ let user_setup () : Factory.setup =
(* --- WP Computer (main entry points) --- *)
(* -------------------------------------------------------------------------- *)
-class type t =
- object
- method model : WpContext.model
- method compute_ip : Property.t -> Wpo.t Bag.t
- method compute_call : stmt -> Wpo.t Bag.t
- method compute_main :
- ?fct:functions ->
- ?bhv:string list ->
- ?prop:string list ->
- unit -> Wpo.t Bag.t
- end
-
let create
?dump ?legacy
?(setup: Factory.setup option)
?(driver: Factory.driver option)
- () : t =
+ () : Wpo.generator =
let default f = function Some v -> v | None -> f () in
let dump = default Wp_parameters.Dump.get dump in
let legacy = default Wp_parameters.Dump.get legacy in
diff --git a/src/plugins/wp/Generator.mli b/src/plugins/wp/Generator.mli
index 18e2e5987911a15119987f714a7eae5cfa1d10e4..fc70c5d2fed6f9d4361d3f53313b271b5dcd990e 100644
--- a/src/plugins/wp/Generator.mli
+++ b/src/plugins/wp/Generator.mli
@@ -18,7 +18,7 @@
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
-(**************************************************************************)
+(*****************************************t*********************************)
open Cil_types
open Wp_parameters
@@ -30,23 +30,11 @@ open Wp_parameters
(** Compute model setup from command line options. *)
val user_setup : unit -> Factory.setup
-class type t =
- object
- method model : WpContext.model
- method compute_ip : Property.t -> Wpo.t Bag.t
- method compute_call : stmt -> Wpo.t Bag.t
- method compute_main :
- ?fct:functions ->
- ?bhv:string list ->
- ?prop:string list ->
- unit -> Wpo.t Bag.t
- end
-
val create :
?dump:bool ->
?legacy:bool ->
?setup:Factory.setup ->
?driver:Factory.driver ->
- unit -> t
+ unit -> Wpo.generator
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index b5be8ba4fe25d91432e1a7a36efed1b5cedf0998..ca2827bdb96d767be642edb0e561d19c1244332e 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -99,7 +99,7 @@ PLUGIN_CMO:= \
Factory \
cfgInit cfgAnnot cfgCalculus \
calculus cfgDump cfgWP \
- wpGenerator \
+ wpGenerator cfgGenerator \
Generator register VC
PLUGIN_CMI:=
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0350785f9871ca9c931ad2e0e8aae4d1455ac602
--- /dev/null
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- New WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+let generators = WpContext.MINDEX.create 1
+
+let generator setup driver =
+ let model = Factory.instance setup driver in
+ try WpContext.MINDEX.find generators model
+ with Not_found ->
+ let module VCG = (val CfgWP.vcgen setup driver) in
+ let module WP = CfgCalculus.Make(VCG) in
+ let generator : Wpo.generator =
+ object
+ method model = model
+ method compute_ip _ = Bag.empty
+ method compute_call _ = Bag.empty
+ method compute_main ?fct ?bhv ?prop () =
+ ignore fct ;
+ ignore bhv ;
+ ignore prop ;
+ Bag.empty
+ end in
+ WpContext.MINDEX.add generators model generator ;
+ generator
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgGenerator.mli b/src/plugins/wp/cfgGenerator.mli
new file mode 100644
index 0000000000000000000000000000000000000000..16461afeba1282f24d982868a9fc3e108dfb662f
--- /dev/null
+++ b/src/plugins/wp/cfgGenerator.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- New WP Computer (main entry points) --- *)
+(* -------------------------------------------------------------------------- *)
+
+val generator : Factory.setup -> Factory.driver -> Wpo.generator
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 9eb93eac1055cb55ef9951b1d52f650859621bdd..4f563fae4490360a834009af6c8ee6d89b6513d2 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1407,7 +1407,7 @@ struct
Wpo.VC_Lemma.depends = l.lem_depends ;
Wpo.VC_Lemma.lemma = def ;
Wpo.VC_Lemma.sequent = None ;
- } in
+ } in
let index = match LogicUsage.section_of_lemma l.lem_name with
| LogicUsage.Toplevel _ -> Wpo.Axiomatic None
| LogicUsage.Axiomatic a -> Wpo.Axiomatic (Some a.ax_name) in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index fde027b2692c9544934618f18dbe15a0a25263f7..50d2653fc068d1a4e4a12bff0f26c7796cbe2341 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -1010,3 +1010,21 @@ let get_files w =
) results []
in
descr_files @ result_files
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type generator =
+ object
+ method model : WpContext.model
+ method compute_ip : Property.t -> t Bag.t
+ method compute_call : stmt -> t Bag.t
+ method compute_main :
+ ?fct:Wp_parameters.functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index fa6d1c337f4055a02c22da886ac0b2e353334be4..753c1c38369621e2aa998895cbe845c829862a6e 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -210,3 +210,21 @@ val pp_goal_flow : Format.formatter -> t -> unit
(** Dynamically exported. *)
val prover_of_name : string -> prover option
+
+(* -------------------------------------------------------------------------- *)
+(* --- Generators --- *)
+(* -------------------------------------------------------------------------- *)
+
+class type generator =
+ object
+ method model : WpContext.model
+ method compute_ip : Property.t -> t Bag.t
+ method compute_call : stmt -> t Bag.t
+ method compute_main :
+ ?fct:Wp_parameters.functions ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t Bag.t
+ end
+
+(* -------------------------------------------------------------------------- *)