From e52eea9fced0a00d7551b931a34d204a1f1cb925 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 10 Apr 2020 09:40:31 +0200
Subject: [PATCH] [wp] Assigned do not considers formal and globals
---
src/plugins/wp/MemVar.ml | 86 +++++++++++++++++++---------------------
1 file changed, 40 insertions(+), 46 deletions(-)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index e82c635975b..18b4f8959f7 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -736,26 +736,18 @@ struct
Set( v2 , update v1 ofs v )
| _ -> failwith "MemVar stored on a non MemVar location"
- let memvar_set_init seq l v =
- match l with
- | Ref x -> noref ~op:"write to" x
- | Val((CREF|CVAL),x,ofs) ->
- let v1 = get_init_term seq.pre x in
- let v2 = get_init_term seq.post x in
- Set( v2 , update_init v1 ofs v )
- | _ -> failwith "MemVar initialize on a non MemVar location"
-
+ let memvar_set_init seq x ofs v =
+ if x.vformal || x.vglob then []
+ else
+ let v1 = get_init_term seq.pre x in
+ let v2 = get_init_term seq.post x in
+ [ Set( v2 , update_init v1 ofs v ) ]
let stored seq obj l v = match l with
| Ref x -> noref ~op:"write to" x
- | Val((CREF|CVAL),x,_) ->
- let init =
- if not (x.vformal || x.vglob) then
- [ memvar_set_init seq l (Cvalues.initialized_obj obj) ]
- else
- []
- in
- (memvar_stored seq obj l v) :: init
+ | Val((CREF|CVAL),x,ofs) ->
+ let init = Cvalues.initialized_obj obj in
+ (memvar_stored seq obj l v) :: (memvar_set_init seq x ofs init)
| Val((CTXT|CARR|HEAP) as m,x,ofs) ->
M.stored (mseq_of_seq seq) obj (mloc_of_path m x ofs) v
| Loc l ->
@@ -1259,40 +1251,42 @@ struct
(* -------------------------------------------------------------------------- *)
let rec monotonic_initialized seq obj x ofs =
- match obj with
- | C_int _ | C_float _ | C_pointer _ ->
- p_imply
- (p_bool (access_init (get_init_term seq.pre x) ofs))
- (p_bool (access_init (get_init_term seq.post x) ofs))
- | C_array { arr_flat=flat ; arr_element=t } ->
- let size = match flat with
- | None -> unsized_array ()
- | Some { arr_size } -> arr_size
- in
- let low = (e_int 0) in
- let up = (e_int (size-1)) in
- let v = Lang.freshvar ~basename:"i" Lang.t_int in
- let hyp = p_and (p_leq low (e_var v)) (p_leq (e_var v) up) in
- let obj = Ctypes.object_of t in
- let ofs = ofs @ [ Shift(obj, e_var v) ] in
- let sub = monotonic_initialized seq obj x ofs in
- Lang.F.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
- monotonic_initialized seq obj x ofs
- in
- Lang.F.p_conj (List.map mk_pred ci.cfields)
+ if x.vformal || x.vglob then p_true
+ else
+ match obj with
+ | C_int _ | C_float _ | C_pointer _ ->
+ p_imply
+ (p_bool (access_init (get_init_term seq.pre x) ofs))
+ (p_bool (access_init (get_init_term seq.post x) ofs))
+ | C_array { arr_flat=flat ; arr_element=t } ->
+ let size = match flat with
+ | None -> unsized_array ()
+ | Some { arr_size } -> arr_size
+ in
+ let low = (e_int 0) in
+ let up = (e_int (size-1)) in
+ let v = Lang.freshvar ~basename:"i" Lang.t_int in
+ let hyp = p_and (p_leq low (e_var v)) (p_leq (e_var v) up) in
+ let obj = Ctypes.object_of t in
+ let ofs = ofs @ [ Shift(obj, e_var v) ] in
+ let sub = monotonic_initialized seq obj x ofs in
+ Lang.F.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
+ monotonic_initialized seq obj x ofs
+ in
+ Lang.F.p_conj (List.map mk_pred ci.cfields)
let memvar_assigned seq obj loc v =
match loc with
| Ref x -> noref ~op:"write to" x
| Val((CREF|CVAL),x,ofs) ->
let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj)) in
- (memvar_set_init seq loc init) ::
+ (memvar_stored seq obj loc v) ::
Assert(monotonic_initialized seq obj x ofs) ::
- [ memvar_stored seq obj loc v ]
+ (memvar_set_init seq x ofs init)
| _ -> failwith "MemVar assigned on a non MemVar location"
let assigned_loc seq obj = function
@@ -1339,8 +1333,8 @@ struct
let ofs = ofs_shift elt (e_var k) ofs in
let obj_x = Ctypes.object_of x.vtype in
let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj_x)) in
- (memvar_set_init seq (Val(m,x,[])) init) ::
Assert(monotonic_initialized seq obj_x x []) ::
+ (memvar_set_init seq x [] init) @
(assigned_genset seq [k] m x ofs p)
let assigned_descr seq obj xs l p =
@@ -1353,8 +1347,8 @@ struct
| Val((CVAL|CREF) as m,x,ofs) ->
let obj_x = Ctypes.object_of x.vtype in
let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj_x)) in
- (memvar_set_init seq (Val(m,x,[])) init) ::
Assert(monotonic_initialized seq obj_x x []) ::
+ (memvar_set_init seq x [] init) @
(assigned_genset seq xs m x ofs p)
let assigned seq obj = function
--
GitLab