diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 6bc07d269978a2d81bda2d34c8628238f6d5184f..668d7573413f311db2bc44cf9e8ec2512c0946a0 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -31,7 +31,8 @@ type behavior = {
bhv_requires: WpPropId.pred_info list ;
bhv_ensures: WpPropId.pred_info list ;
bhv_exits: WpPropId.pred_info list ;
- bhv_assigns: WpPropId.assigns_full_info ;
+ bhv_post_assigns: WpPropId.assigns_full_info ;
+ bhv_exit_assigns: WpPropId.assigns_full_info ;
}
let normalize_assumes kf ki h =
@@ -73,35 +74,47 @@ let normalize_froms kf ki froms =
| Kstmt s -> L.labels_stmt_assigns kf s in
L.preproc_assigns labels froms
-let normalize_assigns kf ki bhv ~active = function
- | WritesAny -> WpPropId.empty_assigns_info
+let normalize_assigns kf ki has_exit bhv ~active = function
+ | WritesAny ->
+ WpPropId.empty_assigns_info, WpPropId.empty_assigns_info
| Writes froms ->
- let aid = match ki with
- | Kglobal -> WpPropId.mk_fct_assigns_id kf bhv Normal froms
- | Kstmt s -> WpPropId.mk_stmt_assigns_id kf s active bhv froms in
- match aid with
- | None -> WpPropId.empty_assigns_info
- | Some id ->
- let assigns = normalize_froms kf ki froms in
- let desc = match ki with
- | Kglobal -> WpPropId.mk_kf_assigns_desc assigns
- | Kstmt s -> WpPropId.mk_stmt_assigns_desc s assigns
- in WpPropId.mk_assigns_info id desc
+ let aid_post, aid_exit = match ki with
+ | Kglobal ->
+ WpPropId.mk_fct_assigns_id kf has_exit bhv Normal froms,
+ WpPropId.mk_fct_assigns_id kf has_exit bhv Exits froms
+ | Kstmt s ->
+ WpPropId.mk_stmt_assigns_id kf s active bhv froms,
+ WpPropId.mk_stmt_assigns_id kf s active bhv []
+ in
+ let make_assigns_info aid =
+ match aid with
+ | None -> WpPropId.empty_assigns_info
+ | Some id ->
+ let assigns = normalize_froms kf ki froms in
+ let desc = match ki with
+ | Kglobal -> WpPropId.mk_kf_assigns_desc assigns
+ | Kstmt s -> WpPropId.mk_stmt_assigns_desc s assigns
+ in WpPropId.mk_assigns_info id desc
+ in
+ make_assigns_info aid_post, make_assigns_info aid_exit
let get_requires kf ki bhv =
List.map (normalize_pre kf ki bhv) bhv.b_requires
-let get_behavior kf ki ~active bhv =
+let get_behavior kf ki has_exit ~active bhv =
let pre_cond = normalize_pre kf ki bhv in
let post_cond tk (kind,ip) =
if kind = tk then Some (normalize_post kf ki bhv tk ip) else None in
- let assigns = normalize_assigns kf ki bhv ~active bhv.b_assigns in
+ let p_asgn, e_asgn =
+ normalize_assigns kf ki has_exit bhv ~active bhv.b_assigns
+ in
{
bhv_assumes = List.map pre_cond bhv.b_assumes;
bhv_requires = List.map pre_cond bhv.b_requires;
bhv_ensures = List.filter_map (post_cond Normal) bhv.b_post_cond ;
bhv_exits = List.filter_map (post_cond Exits) bhv.b_post_cond ;
- bhv_assigns = assigns ;
+ bhv_post_assigns = p_asgn ;
+ bhv_exit_assigns = e_asgn ;
}
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 44a71ff4ed8840b7b42011dbdf9ad74554a35ac3..9f27aab9ad44e9f9d29a587d92f9fed833d9d500 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -37,12 +37,14 @@ type behavior = {
bhv_requires: pred_info list ;
bhv_ensures: pred_info list ;
bhv_exits: pred_info list ;
- bhv_assigns: assigns_full_info ;
+ bhv_post_assigns: assigns_full_info ;
+ bhv_exit_assigns: assigns_full_info ;
}
val get_requires : kernel_function -> kinstr -> funbehavior -> pred_info list
-val get_behavior : kernel_function -> kinstr -> active:string list ->
- funbehavior -> behavior
+val get_behavior :
+ kernel_function -> kinstr -> bool -> active:string list -> funbehavior ->
+ behavior
val get_preconditions : kernel_function -> pred_info list
val get_complete_behaviors : kernel_function -> pred_info list
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 24527f5f773630af9474ca1b0953746e467a7a0f..e8d0582346f29b867b37a7c1752cc96ff0894dfe 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -121,6 +121,37 @@ struct
module I = CfgInit.Make(W)
+ module Reachable_call : sig
+ val has_reachable_call: Cfg.automaton -> vertex -> bool
+ end
+ =
+ struct
+ exception Found_call
+
+ type reachability_env = {
+ table: unit Vhash.t ;
+ cfg: Cfg.automaton ;
+ }
+
+ let rec has_reachable_call cfg v =
+ let env = { table = Vhash.create 32 ; cfg } in
+ try reachable_call_by_cfg env v ; false
+ with Found_call -> true
+
+ and reachable_call_by_cfg env a =
+ try Vhash.find env.table a
+ with Not_found ->
+ Vhash.add env.table a () ;
+ List.iter (transition env) (G.succ_e env.cfg.graph a)
+
+ and transition env (_,edge,dst) =
+ reachable_call_by_cfg env dst ;
+ match edge.edge_transition with
+ | Instr ((Local_init(_,ConsInit _, _)| Call _), _) -> raise Found_call
+ | _ -> ()
+
+ end
+
(* --- Traversal Environment --- *)
type env = {
@@ -317,7 +348,7 @@ struct
let body env ~ensures ~exits w =
let rw = List.fold_right (prove_property env) ensures w in
- let rk = List.fold_right (prove_property env) exits w in
+ let rk = List.fold_right (prove_property env) exits env.wk in
Vhash.add env.wp env.cfg.return_point (Some rw) ;
env.wk <- rk ;
wp env env.cfg.entry_point
@@ -325,16 +356,18 @@ struct
(* Putting everything together *)
let compute ~mode ~props =
let kf = mode.kf in
+ let cfg = Cfg.get_automaton kf in
+ let has_exit = Reachable_call.has_reachable_call cfg (cfg.entry_point) in
let env = {
mode ; props ;
- cfg = Cfg.get_automaton kf ;
+ cfg ;
we = W.new_env kf ;
wp = Vhash.create 32 ;
wk = W.empty ;
} in
let xs = Kernel_function.get_formals kf in
let req = default_requires mode kf in
- let bhv = CfgAnnot.get_behavior kf Kglobal ~active:[] mode.bhv in
+ let bhv = CfgAnnot.get_behavior kf Kglobal has_exit ~active:[] mode.bhv in
env.we ,
(* global init *)
@@ -357,8 +390,11 @@ struct
~exits:bhv.bhv_exits @@
(* frame-out *)
W.label env.we None Clabels.post @@
+ (fun t ->
+ if not has_exit then env.wk <- t
+ else env.wk <- prove_assigns env bhv.bhv_exit_assigns t ;
+ prove_assigns env bhv.bhv_post_assigns t) @@
W.scope env.we xs SC_Frame_out @@
- prove_assigns env bhv.bhv_assigns @@
(* wp-end *)
W.empty
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 1e0f4006807ef333e08be1f81b91c615d293974a..4e89b7789319d5a180885cd20e5636def3ed117d 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -302,7 +302,8 @@ let add_stmt_assigns_goal config s active acc b l_post = match b.b_assigns with
let add_fct_assigns_goal config acc tkind b = match b.b_assigns with
| WritesAny -> acc
| Writes assigns ->
- let id = WpPropId.mk_fct_assigns_id config.kf b tkind assigns in
+ let has_exit = Cil2cfg.has_exit (Cil2cfg.get config.kf) in
+ let id = WpPropId.mk_fct_assigns_id config.kf has_exit b tkind assigns in
match id with
| None -> acc
| Some id ->
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index e8f8f5ad372690f1a62268b13fc6694613dc3b8d..8c55663118844355306ece661ef28d9ba9f4f0e2 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -128,16 +128,16 @@ let mk_bhv_from_id kf ki a bhv from =
let id = Property.ip_of_from kf ki (Property.Id_contract (a,bhv)) from in
mk_prop PKProp (Option.get id)
-let get_kind_for_tk kf tkind = match tkind with
+let get_kind_for_tk tkind has_exit = match tkind with
| Normal ->
- if Cil2cfg.has_exit (Cil2cfg.get kf) then PKAFctOut else PKProp
+ if has_exit then PKAFctOut else PKProp
| Exits -> PKAFctExit
| _ -> assert false
-let mk_fct_from_id kf bhv tkind from =
+let mk_fct_from_id kf kf_has_exit bhv tkind from =
let contract_info = Property.Id_contract(Datatype.String.Set.empty,bhv) in
let id = Property.ip_of_from kf Kglobal contract_info from in
- let kind = get_kind_for_tk kf tkind in
+ let kind = get_kind_for_tk tkind kf_has_exit in
mk_prop kind (Option.get id)
let mk_disj_bhv_id (kf,ki,active,disj) =
@@ -160,9 +160,9 @@ let mk_loop_assigns_id kf s ca a =
let p = Property.ip_of_assigns kf (Kstmt s) ca (Writes a) in
Option.map (mk_prop PKPropLoop) p
-let mk_fct_assigns_id kf b tkind a =
+let mk_fct_assigns_id kf kf_has_exit b tkind a =
let b = Property.Id_contract(Datatype.String.Set.empty,b) in
- let kind = get_kind_for_tk kf tkind in
+ let kind = get_kind_for_tk tkind kf_has_exit in
let p = Property.ip_of_assigns kf Kglobal b (Writes a) in
Option.map (mk_prop kind) p
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 95f6808f4c2794043505bcf24e32e774f483c5ad..149edcd544d68fa26bec31c39518bca0788540be 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -148,8 +148,10 @@ val mk_bhv_from_id :
kernel_function -> kinstr -> string list -> funbehavior ->
from -> prop_id
-(** \from property of function behavior assigns. Must not be [FromAny]. *)
-val mk_fct_from_id : kernel_function -> funbehavior ->
+(** \from property of function behavior assigns. Must not be [FromAny].
+ The boolean indicate whether the function has exit node or not.
+*)
+val mk_fct_from_id : kernel_function -> bool -> funbehavior ->
termination_kind -> from -> prop_id
(** disjoint behaviors property.
@@ -176,8 +178,10 @@ val mk_stmt_assigns_id :
val mk_loop_assigns_id : kernel_function -> stmt -> code_annotation ->
from list -> prop_id option
-(** function assigns *)
-val mk_fct_assigns_id : kernel_function -> funbehavior ->
+(** function assigns
+ The boolean indicate whether the function has exit node or not.
+*)
+val mk_fct_assigns_id : kernel_function -> bool -> funbehavior ->
termination_kind -> from list -> prop_id option
val mk_pre_id : kernel_function -> kinstr -> funbehavior ->
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 195affa7997046ebeebe75c3b00e2d8c1ca733ae..38aca8858461ece782e5e32f03949f5c1bc24131 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -464,7 +464,8 @@ let add_fct_bhv_assigns_hyp acc kf tkind b = match b.b_assigns with
let id = WpPropId.mk_kf_any_assigns_info () in
add_assigns_any acc Ahyp id
| Writes assigns ->
- let id = WpPropId.mk_fct_assigns_id kf b tkind assigns in
+ let has_exit = Cil2cfg.has_exit (Cil2cfg.get kf) in
+ let id = WpPropId.mk_fct_assigns_id kf has_exit b tkind assigns in
match id with
| None ->
let id = WpPropId.mk_kf_any_assigns_info () in