diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2b26ffebd044da5c6c457a48129e865df25515b6..2882e2aa095f96552d3ed0c5e6320f00d4b26d81 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -392,7 +392,7 @@ struct
| Cfield _ , Mfield _ -> 1
| Cfield(f, KValue) , Cfield(g, KValue)
| Cfield(f, KInit) , Cfield(g, KInit) ->
- Fieldinfo.compare f g
+ Fieldinfo.compare f g
| Cfield(_, KInit), Cfield(_, KValue) -> (-1)
| Cfield(_, KValue), Cfield(_, KInit) -> 1
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index e90a204fdaf76799c83dae1f0f417969ec452936..d75334e7c34bab7f89f75f71e3014a4bf242a85f 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -151,17 +151,17 @@ struct
let tau_of_chunk = function
| Var x -> VAR.tau_of_chunk x
| Alloc x -> VALLOC.tau_of_chunk x
- | Init _ -> Qed.Logic.Bool
+ | Init x -> VINIT.tau_of_chunk x
| Mem m -> M.Chunk.tau_of_chunk m
let basename_of_chunk = function
| Var x -> VAR.basename_of_chunk x
| Alloc x -> VALLOC.basename_of_chunk x
- | Init _ -> "VInit"
+ | Init x -> VINIT.basename_of_chunk x
| Mem m -> M.Chunk.basename_of_chunk m
let is_framed = function
| Var x -> VAR.is_framed x
| Alloc x -> VALLOC.is_framed x
- | Init x -> VAR.is_framed x
+ | Init x -> VINIT.is_framed x
| Mem m -> M.Chunk.is_framed m
end
@@ -234,10 +234,10 @@ struct
let join s1 s2 =
Passive.union
(Passive.union
- (Passive.union
- (SIGMA.join s1.vars s2.vars)
- (ALLOC.join s1.alloc s2.alloc))
- (M.Sigma.join s1.mem s2.mem))
+ (Passive.union
+ (SIGMA.join s1.vars s2.vars)
+ (ALLOC.join s1.alloc s2.alloc))
+ (M.Sigma.join s1.mem s2.mem))
(INIT.join s1.init s2.init)
let get s = function
@@ -340,19 +340,19 @@ struct
let domain s =
Heap.Set.union
(Heap.Set.union
- (Heap.Set.union
- (domain_var (SIGMA.domain s.vars))
- (domain_alloc (ALLOC.domain s.alloc)))
- (domain_mem (M.Sigma.domain s.mem)))
+ (Heap.Set.union
+ (domain_var (SIGMA.domain s.vars))
+ (domain_alloc (ALLOC.domain s.alloc)))
+ (domain_mem (M.Sigma.domain s.mem)))
(domain_init (INIT.domain s.init))
let writes s =
Heap.Set.union
(Heap.Set.union
- (Heap.Set.union
- (domain_var (SIGMA.writes {pre=s.pre.vars;post=s.post.vars}))
- (domain_alloc (ALLOC.writes {pre=s.pre.alloc;post=s.post.alloc})))
- (domain_mem (M.Sigma.writes {pre=s.pre.mem;post=s.post.mem})))
+ (Heap.Set.union
+ (domain_var (SIGMA.writes {pre=s.pre.vars;post=s.post.vars}))
+ (domain_alloc (ALLOC.writes {pre=s.pre.alloc;post=s.post.alloc})))
+ (domain_mem (M.Sigma.writes {pre=s.pre.mem;post=s.post.mem})))
(domain_init (INIT.writes {pre=s.pre.init;post=s.post.init}))
let pretty fmt s =
@@ -424,10 +424,6 @@ struct
let c = match V.param x with ByRef -> Iref x | _ -> Ivar x in
m := set_chunk (e_var v) c !m
) s.vars ;
- INIT.iter (fun x v ->
- let c = match V.param x with ByRef -> Iref x | _ -> Ivar x in
- m := set_chunk (e_var v) c !m
- ) s.init ;
{ svar = !m ; smem = M.state s.mem }
let ilval = function
@@ -477,7 +473,7 @@ struct
let m = F.e_setfield v2 fd f1 in
Bag.concat upd (diff lv v1 m)
| (Lang.Cfield (_fi, KInit) as _fd ,_f2) :: _fvs ->
- assert false (* TODO *)
+ assert false (* TODO *)
| (Lang.Mfield _,_)::_ -> Bag.elt (Mstore(lv,v2))
| [] -> Bag.empty
@@ -732,6 +728,24 @@ struct
(* --- Memory Store --- *)
(* -------------------------------------------------------------------------- *)
+ let rec initialized_value value obj =
+ match obj with
+ | C_int _ | C_float _ | C_pointer _ -> value
+ | C_comp ci ->
+ let make_initialized_term f =
+ let obj = Ctypes.object_of f.ftype in
+ Cfield (f, KInit), initialized_value value obj
+ in
+ let ts = List.map make_initialized_term ci.cfields in
+ Lang.F.e_record ts
+ | C_array _ as arr ->
+ let obj = Ctypes.object_of_array_elem arr in
+ let t = initialized_value value obj in
+ Lang.F.e_const Lang.t_int t
+
+ let initialized_obj = initialized_value e_true
+ let uninitialized_obj = initialized_value e_false
+
let stored seq obj l v = match l with
| Ref x -> noref ~op:"write to" x
| Val((CREF|CVAL),x,ofs) ->
@@ -741,7 +755,8 @@ struct
if not (x.vformal || x.vglob) then
let i1 = get_init_term seq.pre x in
let i2 = get_init_term seq.post x in
- [ Set( i2 , update_init i1 ofs F.e_true ) ]
+ let init = initialized_obj obj in
+ [ Set( i2 , update_init i1 ofs init ) ]
else
[]
in
@@ -1017,33 +1032,31 @@ struct
(* --- Initialized --- *)
(* -------------------------------------------------------------------------- *)
- let rec make_initialized_value value sigma obj x ofs =
+ let rec initialized_loc sigma obj x ofs =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- e_eq value (access_init (get_init_term sigma x) ofs)
+ e_eq e_true (access_init (get_init_term sigma x) ofs)
| C_array { arr_element=t ; arr_flat=flat } ->
- let v = Lang.freshvar ~basename:"i" Lang.t_int in
- let hyp = match flat with
- | None -> e_true
- | Some { arr_size=size } ->
- let open Lang.F in
- e_and [ (e_leq e_zero (e_var v)) ; (e_leq (e_var v) (e_int size)) ]
- in
- let hyp = p_bool hyp in
- let obj = Ctypes.object_of t in
- let ofs = ofs @ [ Shift(obj, e_var v) ] in
- let sub = p_bool (make_initialized_value value sigma obj x ofs) in
- e_prop (p_forall [v] (p_imply hyp sub))
+ let v = Lang.freshvar ~basename:"i" Lang.t_int in
+ let hyp = match flat with
+ | None -> e_true
+ | Some { arr_size=size } ->
+ let open Lang.F in
+ e_and [ (e_leq e_zero (e_var v)) ;
+ (e_leq (e_var v) (e_int (size-1))) ]
+ in
+ let hyp = p_bool hyp in
+ let obj = Ctypes.object_of t in
+ let ofs = ofs @ [ Shift(obj, e_var v) ] in
+ let sub = p_bool (initialized_loc sigma obj x ofs) in
+ e_prop (p_forall [v] (p_imply hyp sub))
| C_comp ci ->
- let mk_pred f =
- let obj = Ctypes.object_of f.ftype in
- let ofs = ofs @ [Field f] in
- make_initialized_value value sigma obj x ofs
- in
- Lang.F.e_and (List.map mk_pred ci.cfields)
-
- let make_initialized = make_initialized_value e_true
- let make_uninitialized = make_initialized_value e_false
+ let mk_pred f =
+ let obj = Ctypes.object_of f.ftype in
+ let ofs = ofs @ [Field f] in
+ initialized_loc sigma obj x ofs
+ in
+ Lang.F.e_and (List.map mk_pred ci.cfields)
let initialized sigma l =
match l with
@@ -1052,33 +1065,33 @@ struct
| Ref _ -> p_true
| Loc l -> M.initialized sigma.mem (Rloc(obj,l))
| Val(m,x,p) ->
- if (x.vformal || x.vglob) then
- p_true
- else if is_heap_allocated m then
- M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
- else
- p_bool (make_initialized sigma obj x p)
+ if (x.vformal || x.vglob) then
+ p_true
+ else if is_heap_allocated m then
+ M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
+ else
+ p_bool (initialized_loc sigma obj x p)
end
| Rrange(l,elt,a,b) ->
begin match l with
| Ref x -> noref ~op:"valid sub-range of" x
| Loc l -> M.initialized sigma.mem (Rrange(l,elt,a,b))
| Val(_m,_x,_p) -> p_false
- (*match a,b with
- | Some ka,Some kb ->
- begin
- try
- F.p_imply (F.p_leq ka kb)
- (valid_range_path sigma acs m x p (elt,ka,kb))
- with ShiftMismatch ->
- if is_heap_allocated m then
- let l = mloc_of_loc l in
- M.valid sigma.mem acs (Rrange(l,elt,a,b))
- else shift_mismatch l
- end
- | _ ->
- Warning.error "Validity of infinite range @[%a.(%a..%a)@]"
- pretty l Vset.pp_bound a Vset.pp_bound b*)
+ (*match a,b with
+ | Some ka,Some kb ->
+ begin
+ try
+ F.p_imply (F.p_leq ka kb)
+ (valid_range_path sigma acs m x p (elt,ka,kb))
+ with ShiftMismatch ->
+ if is_heap_allocated m then
+ let l = mloc_of_loc l in
+ M.valid sigma.mem acs (Rrange(l,elt,a,b))
+ else shift_mismatch l
+ end
+ | _ ->
+ Warning.error "Validity of infinite range @[%a.(%a..%a)@]"
+ pretty l Vset.pp_bound a Vset.pp_bound b*)
end
@@ -1094,7 +1107,7 @@ struct
| TComp({ cfields },_,_) ->
F.p_all
(fun fd ->
- forall_pointers phi (e_getfield v (Cfield (fd, KValue))) fd.ftype)
+ forall_pointers phi (e_getfield v (Cfield (fd, KValue))) fd.ftype)
cfields
| TArray(elt,_,_,_) ->
let k = Lang.freshvar Qed.Logic.Int in
@@ -1155,12 +1168,12 @@ struct
match scope with
| Leave -> []
| Enter ->
- let xs = List.filter (fun v -> not v.vformal && not v.vglob) xs in
- let i_out = seq.post in
- let uninitialized v =
- Lang.F.p_bool (make_uninitialized i_out (Ctypes.object_of v.vtype) v [])
- in
- List.map uninitialized xs
+ let xs = List.filter (fun v -> not v.vformal && not v.vglob) xs in
+ let uninitialized v =
+ let uninit_value = uninitialized_obj (Ctypes.object_of v.vtype) in
+ Lang.F.p_equal (access_init (get_init_term seq.post v) []) uninit_value
+ in
+ List.map uninitialized xs
let scope seq scope xs =
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 01886aa619b932eda09448760dadffd4d58c4072..2ce0d949afd6bb95775b1d73357f7401550a04c0 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -557,14 +557,14 @@ let rec of_term ~cnv expected t : Why3.Term.term =
let s = Lang.name_of_field f in
match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)) with
| ls ->
- begin match tau with
- | Prop ->
- Why3.Term.t_equ
- (Why3.Term.t_app ls [of_term' cnv a] (Some Why3.Ty.ty_bool))
- (Why3.Term.t_bool_true)
- | _ ->
- Why3.Term.t_app ls [of_term' cnv a] (of_tau ~cnv tau)
- end
+ begin match tau with
+ | Prop ->
+ Why3.Term.t_equ
+ (Why3.Term.t_app ls [of_term' cnv a] (Some Why3.Ty.ty_bool))
+ (Why3.Term.t_bool_true)
+ | _ ->
+ Why3.Term.t_app ls [of_term' cnv a] (of_tau ~cnv tau)
+ end
| exception Not_found -> why3_failure "Can't find '%s' in why3 namespace" s
end
@@ -931,10 +931,7 @@ class visitor (ctx:context) c =
let id = Why3.Ident.id_fresh (Lang.comp_init_id c) in
let cnv = empty_cnv ctx in
let map (f,tau) =
- let ty_ctr = match of_tau ~cnv tau with
- | None -> Some Why3.Ty.ty_bool
- | t -> t
- in
+ let ty_ctr = of_tau ~cnv tau in
let id = Why3.Ident.id_fresh (Lang.name_of_field f) in
let ls = Why3.Term.create_lsymbol id [ty] ty_ctr in
(Some ls,Why3.Opt.get ty_ctr)