[wp] Initialized: deals with Local_init

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 =

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

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
 

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

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
 
   (* -------------------------------------------------------------------------- *)