diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7698e1df5e9ccfcfd40900f56fa4c7fa14afc0ec..0fd0efdddd6bf3c39b989725d6d069d831dde2ce 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1676,6 +1676,8 @@ src/plugins/wp/calculus.ml: CEA_WP
src/plugins/wp/calculus.mli: CEA_WP
src/plugins/wp/cfgAnnot.ml: CEA_WP
src/plugins/wp/cfgAnnot.mli: CEA_WP
+src/plugins/wp/cfgInfos.ml: CEA_WP
+src/plugins/wp/cfgInfos.mli: CEA_WP
src/plugins/wp/cfgCalculus.ml: CEA_WP
src/plugins/wp/cfgCalculus.mli: CEA_WP
src/plugins/wp/cfgDump.ml: CEA_WP
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 20cfa49ccc1af5984386ab78c5f6230577d7e716..235d396271078e77a6e0cd9d5231e09738511bcf 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -378,6 +378,41 @@ let get_behavior = function
| IPGlobalInvariant _
| IPOther _ -> None
+let get_for_behaviors = function
+ | IPPredicate {ip_kind} ->
+ (match get_pk_behavior ip_kind with None -> [] | Some b -> [b.b_name])
+ | IPBehavior {ib_bhv=b}
+ | IPAllocation {ial_bhv=Id_contract (_, b)}
+ | IPAssigns {ias_bhv=Id_contract (_, b)}
+ | IPFrom {if_bhv=Id_contract (_, b)} -> [b.b_name]
+
+ | IPAllocation {ial_bhv=Id_loop ca}
+ | IPAssigns {ias_bhv=Id_loop ca}
+ | IPFrom {if_bhv=Id_loop ca}
+ | IPCodeAnnot { ica_ca = ca } ->
+ begin
+ match ca.annot_content with
+ | AAssert (bhvs,_)
+ | AInvariant (bhvs,_,_)
+ | AStmtSpec(bhvs,_)
+ | AAssigns(bhvs,_)
+ | AAllocation(bhvs,_) -> bhvs
+ | AVariant _ | APragma _ | AExtended _ -> []
+ end
+
+ | IPAxiom _
+ | IPAxiomatic _
+ | IPExtended _
+ | IPLemma _
+ | IPComplete _
+ | IPDisjoint _
+ | IPDecrease _
+ | IPReachable _
+ | IPPropertyInstance _
+ | IPTypeInvariant _
+ | IPGlobalInvariant _
+ | IPOther _ -> []
+
(* -------------------------------------------------------------------------- *)
(* --- Property Status --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 6ad7e28371f3d73dfba4d67ff5a61f5dd1d98164..6f0b150adb05d0acf4e9a1997c6e97a8f32c163a 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -517,6 +517,7 @@ val get_kinstr: identified_property -> kinstr
val get_kf: identified_property -> kernel_function option
val get_behavior: identified_property -> funbehavior option
val get_names: identified_property -> string list
+val get_for_behaviors: identified_property -> string list
val location: identified_property -> location
(** returns the location of the property.
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index ca2827bdb96d767be642edb0e561d19c1244332e..5fbddfa3c16148ddf51a7f458ace805463df93ec 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -97,7 +97,7 @@ PLUGIN_CMO:= \
filter_axioms Cache ProverWhy3 \
driver prover ProverSearch ProverScript \
Factory \
- cfgInit cfgAnnot cfgCalculus \
+ cfgInit cfgAnnot cfgInfos cfgCalculus \
calculus cfgDump cfgWP \
wpGenerator cfgGenerator \
Generator register VC
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7dd1486b6392c83a551f712d82ae8ec3194d6242
--- /dev/null
+++ b/src/plugins/wp/cfgInfos.ml
@@ -0,0 +1,136 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Cfg = Interpreted_automata
+module Fset = Kernel_function.Set
+module Vhash = Cfg.Vertex.Hashtbl
+module Shash = Cil_datatype.Stmt.Hashtbl
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute Kernel-Function & CFG Infos for WP --- *)
+(* -------------------------------------------------------------------------- *)
+
+type t = {
+ cfg : Cfg.automaton;
+ mutable annots : bool; (* has goals to prove *)
+ mutable doomed : WpPropId.prop_id Bag.t;
+ mutable calls : Kernel_function.Set.t;
+ unreachable : bool Vhash.t ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Getters --- *)
+(* -------------------------------------------------------------------------- *)
+
+let calls infos = infos.calls
+let annots infos = infos.annots
+let doomed infos = infos.doomed
+
+(* -------------------------------------------------------------------------- *)
+(* --- Reachability Analyses --- *)
+(* -------------------------------------------------------------------------- *)
+
+let fixpoint h d f =
+ let rec phi v =
+ try Vhash.find h v
+ with Not_found ->
+ Vhash.add h v d ;
+ let r = f phi v in
+ Vhash.replace h v r ; r
+ in phi
+
+let unreachable infos =
+ let pred = Cfg.G.pred infos.cfg.graph in
+ fixpoint infos.unreachable true
+ begin fun phi v -> List.for_all phi (pred v) end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Selected Properties --- *)
+(* -------------------------------------------------------------------------- *)
+
+let selected ~bhv ~prop pid =
+ (prop = [] || WpPropId.select_by_name prop pid) &&
+ (bhv = [] || WpPropId.select_for_behaviors bhv pid)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Calls --- *)
+(* -------------------------------------------------------------------------- *)
+
+let collect_calls ~bhv stmt =
+ let open Cil_types in
+ match stmt.skind with
+ | Instr(Call(_,fct,_,_)) ->
+ begin
+ match Kernel_function.get_called fct with
+ | Some kf -> Fset.singleton kf
+ | None ->
+ let bhvs = if bhv = [] then [Cil.default_behavior_name] else bhv in
+ List.fold_left
+ (fun fs bhv -> match Dyncall.get ~bhv stmt with
+ | None -> fs
+ | Some(_,kfs) -> List.fold_right Fset.add kfs fs
+ ) Fset.empty bhvs
+ end
+ | Instr(Local_init(x,ConsInit(vf, args, kind), loc)) ->
+ Cil.treat_constructor_as_func
+ (fun _r fct _args _loc ->
+ match Kernel_function.get_called fct with
+ | Some kf -> Fset.singleton kf
+ | None -> Fset.empty)
+ x vf args kind loc
+ | _ -> Fset.empty
+
+(* -------------------------------------------------------------------------- *)
+(* --- Main Collection Pass --- *)
+(* -------------------------------------------------------------------------- *)
+
+let collect kf cfg ?(bhv=[]) ?(prop=[]) () =
+ let infos = {
+ cfg ;
+ annots = false ;
+ doomed = Bag.empty ;
+ calls = Fset.empty ;
+ unreachable = Vhash.create 32 ;
+ } in
+ (* Root Reachability *)
+ let v0 = cfg.entry_point in
+ Vhash.add infos.unreachable v0 false ;
+ (* Stmt Iteration *)
+ Shash.iter
+ (fun stmt (src,_) ->
+ let fs = collect_calls ~bhv stmt in
+ let dead = unreachable infos src in
+ let ca = CfgAnnot.get_code_assertions kf stmt in
+ let pids = List.map fst ca.code_verified in
+ if dead then
+ infos.doomed <- Bag.concat infos.doomed (Bag.list pids)
+ else
+ begin
+ if List.exists (selected ~bhv ~prop) pids
+ then infos.annots <- true ;
+ infos.calls <- Fset.union fs infos.calls ;
+ end
+ ) cfg.stmt_table ;
+ (* Collected Infos *)
+ infos
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a568567c1fc7cd519534b634a36ca1d9ffaa8a6c
--- /dev/null
+++ b/src/plugins/wp/cfgInfos.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Compute Kernel-Function & CFG Infos for WP *)
+
+type t
+
+module Cfg = Interpreted_automata
+
+val collect : Kernel_function.t -> Cfg.automaton ->
+ ?bhv:string list ->
+ ?prop:string list ->
+ unit -> t
+val annots : t -> bool
+val doomed : t -> WpPropId.prop_id Bag.t
+val calls : t -> Kernel_function.Set.t
+val unreachable : t -> Cfg.vertex -> bool
+
+(**************************************************************************)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 8c55663118844355306ece661ef28d9ba9f4f0e2..c84bb0f04daf6d601f130d3f8a4215940038a94c 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -817,6 +817,10 @@ let select_by_name asked_names pid =
let names = user_prop_pid pid in
are_selected_names asked_names names
+let select_for_behaviors bhvs pid =
+ let fors = Property.get_for_behaviors @@ property_of_id pid in
+ List.exists (fun b -> List.mem b fors) bhvs
+
let select_call_pre s_call asked_pre pid =
match pid.p_kind with
| PKPre (_, p_stmt, p_prop) ->
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 149edcd544d68fa26bec31c39518bca0788540be..1a01137e5efb1fb7d91f80b76b99f74fcce9643e 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -62,14 +62,13 @@ val is_smoke_test : prop_id -> bool
(** test if the prop_id does not have a [no_wp:] in its name(s). *)
val select_default : prop_id -> bool
-(** test if the prop_id has to be selected for the asked name.
- Also returns a debug message to explain then answer. Includes
- a test for [no_wp:]. *)
+(** test if the prop_id has to be selected for the asked names. *)
val select_by_name : string list -> prop_id -> bool
-(** test if the prop_id has to be selected when we want to select the call
- * precondition the the [stmt] call (None means all the call preconditions).
- * Also returns a debug message to explain then answer. *)
+(** test if the prop_id has to be selected for the asked behavior names. *)
+val select_for_behaviors : string list -> prop_id -> bool
+
+(** test if the prop_id has to be selected when we want to select the call. *)
val select_call_pre : stmt -> Property.t option -> prop_id -> bool
(*----------------------------------------------------------------------------*)