diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index be4aaa052a4dbdf880a9cca401901a3ec7cb8ed4..80b3fbb8928bcae0edacd44e7435673effdea0ae 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -443,14 +443,16 @@ struct
~severe:false ~effect:"Skip initializer"
(fun () ->
let l = lval sigma lv in
- match init with
- | Some e ->
- let v = M.load sigma obj l in
- p_equal (val_of_exp sigma e) (cval v)
- | None -> is_zero sigma obj l
+ let value_hyp = match init with
+ | Some e ->
+ let v = M.load sigma obj l in
+ p_equal (val_of_exp sigma e) (cval v)
+ | None -> is_zero sigma obj l
+ in
+ value_hyp, (M.initialized sigma (Rloc(obj, l)))
) () in
match outcome with
- | Warning.Failed warn -> warn , F.p_true
+ | Warning.Failed warn -> warn , (F.p_true, F.p_true)
| Warning.Result(warn , hyp) -> warn , hyp
let init_range ~sigma lv typ a b value =
@@ -460,14 +462,16 @@ struct
(fun () ->
let l = lval sigma lv in
let e = Extlib.opt_map (exp sigma) value in
- is_exp_range sigma l obj (e_bigint a) (e_bigint b) e
+ let a = e_bigint a and b = e_bigint b in
+ (is_exp_range sigma l obj a b e),
+ (M.initialized sigma (Rrange(l, obj, Some a, Some b)))
) () in
match outcome with
- | Warning.Failed warn -> warn , F.p_true
+ | Warning.Failed warn -> warn , (F.p_true, F.p_true)
| Warning.Result(warn , hyp) -> warn , hyp
- type warned_hyp = Warning.Set.t * Lang.F.pred
+ type warned_hyp = Warning.Set.t * (Lang.F.pred * Lang.F.pred)
(* Hypothesis for initialization of one variable *)
let rec init_variable ~sigma lv init acc =
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 102135a390c059ec2ecddaa30e0e355e555ff18d..cff7c98d4b931c4fe4281801d3f541d0d6058225 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1190,7 +1190,9 @@ struct
match scope with
| Leave -> []
| Enter ->
- let xs = List.filter (fun v -> not v.vformal && not v.vglob) xs in
+ let xs = List.filter
+ (fun v -> not v.vformal && not v.vglob && not v.vdefined) xs
+ in
let uninitialized v =
let value = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in
Lang.F.p_equal (access_init (get_init_term seq.post v) []) value
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index e5c252e0076a78c4833cb29d0d7ed58bdbd14a0b..112b10ad0b721a906ef2a12abc6798d69f6b2099 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -598,17 +598,23 @@ sig
val unchanged : M.sigma -> M.sigma -> varinfo -> pred
(** Express that a given variable has the same value in two memory states. *)
- type warned_hyp = Warning.Set.t * pred
-
- val init : sigma:M.sigma -> varinfo -> init option -> warned_hyp list
- (** Express that some variable has some initial value at the
- given memory state.
-
- Remark: [None] initializer are interpreted as zeroes. This is consistent
- with the [init option] associated with global variables in CIL,
- for which the default initializer are zeroes. There is no
- [init option] value associated with local initializers.
- *)
+ type warned_hyp = Warning.Set.t * (pred * pred)
+
+ val init :
+ sigma:M.sigma -> varinfo -> init option -> warned_hyp list
+ (** Express that some variable has some initial value at the
+ given memory state. The first predicate states the value,
+ the second, the initialization status.
+
+ Note: we DO NOT merge values and initialization status
+ hypotheses as the factorization performed by Qed can make
+ predicates too hard to simplify later.
+
+ Remark: [None] initializer are interpreted as zeroes. This is consistent
+ with the [init option] associated with global variables in CIL,
+ for which the default initializer are zeroes. There is no
+ [init option] value associated with local initializers.
+ *)
end
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 28aaa51e928def28bc856f4e00b73a7a3beb52c5..4272a3333deb1d013d8d4681454ad19a04edd7b2 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -416,7 +416,10 @@ struct
let here = Sigma.create () in
let next = Sigma.create () in
(*TODO: make something of warnings *)
- let hyp = Lang.F.p_all snd (C.init ~sigma:next vi (Some init)) in
+ let init = C.init ~sigma:next vi (Some init) in
+ let hyp_value = Lang.F.p_all (fun (_, h) -> fst h) init in
+ let hyp_init = Lang.F.p_all (fun (_, h) -> snd h) init in
+ let hyp = Lang.F.p_and hyp_init hyp_value in
effect (env @: Clabels.here) (Cfg.E.create {pre=here; post=next} hyp) (env @: Clabels.next)
| Skip _ | Code_annot _ -> goto (env @: Clabels.here) (env @: Clabels.next)
@@ -669,7 +672,10 @@ struct
let cfg_init = Globals.Vars.fold_in_file_order
(fun var initinfo cfg ->
if var.vstorage = Extern then cfg else
- let h = Lang.F.p_all snd (C.init ~sigma:sinit var initinfo.init) in
+ let init = C.init ~sigma:sinit var initinfo.init in
+ let hvalue = Lang.F.p_all (fun (_, h) -> fst h) init in
+ let hinit = Lang.F.p_all (fun (_, h) -> snd h) init in
+ let h = Lang.F.p_and hvalue hinit in
let h = Cfg.P.create
(Cfg.Node.Map.add ninit sinit Cfg.Node.Map.empty)
h
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index f5006fd95ba3ffa91d98ab0e8eee3dbaa053259a..837791824a5086d954ccdae241bc7af4147f1e6e 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -250,7 +250,9 @@ struct
let assume_vcs ?descr ?filter ?init whs vc =
List.fold_left
- (fun vc (warn,hyp) -> assume_vc ?descr ?filter ?init ~warn [hyp] vc)
+ (fun vc (warn, (hvalue, hinit)) ->
+ let vc = assume_vc ?descr ?filter ?init ~warn [hvalue] vc in
+ assume_vc ?descr ?filter ?init ~warn [hinit] vc)
vc whs
(* -------------------------------------------------------------------------- *)