diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index 2a089e418a406d92bb4eab9cd2ed4d275108a84f..3e4a54ca47cbf8dae2803864a313f97290f61f20 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -94,7 +94,7 @@ struct
| C_float _ -> is_zero_float (M.load sigma obj l)
| C_pointer _ -> is_zero_ptr (M.load sigma obj l)
| C_comp { cfields = None } ->
- Wp_parameters.fatal "0-initialization of an opaque structure"
+ p_true (* cannot say anything interesting here *)
| C_comp { cfields = Some fields } ->
p_all
(fun f -> is_zero sigma (Ctypes.object_of f.ftype) (M.field l f))
@@ -451,7 +451,17 @@ struct
p_equal (val_of_exp sigma e) (cval v)
| None -> is_zero sigma obj l
in
- value_hyp, (M.initialized sigma (Rloc(obj, l)))
+ let init_hyp = match init with
+ | Some { enode = Lval lv_init }
+ when Cil.(isStructOrUnionType @@ typeOfLval lv_init) ->
+ let l_initializer = lval sigma lv_init in
+ p_equal
+ (M.load_init sigma obj l)
+ (M.load_init sigma obj l_initializer)
+ | _ ->
+ M.initialized sigma (Rloc(obj, l))
+ in
+ value_hyp, init_hyp
) () in
match outcome with
| Warning.Failed warn -> warn , (F.p_true, F.p_true)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 5c8b21c9784d4b7ad35602673189459350cb5cae..d26aee33e7d63313fd60a43d4d65ceaa2d7354db 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -133,6 +133,9 @@ and init_comp_value value ci =
let initialized_obj = init_value e_true
let uninitialized_obj = init_value e_false
+let always_initialized x =
+ (x.vformal || x.vglob) && not @@ Cil.isStructOrUnionType x.vtype
+
(* -------------------------------------------------------------------------- *)
(* --- Length of empty compinfos --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 01fd0ed8bdff0d9922e7dca7b4f84b41701d5838..c9d70fa788fe5b589937095d80429bcb20a74083 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -99,6 +99,7 @@ val logic_constant : logic_constant -> term
val constant_exp : exp -> term
val constant_term : Cil_types.term -> term
+val always_initialized: varinfo -> bool
val initialized_obj: c_object -> term
val uninitialized_obj: c_object -> term
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index b69ac15ba6b43f85c140595c3a0889cb83b85dac..e4fbf4526f69b2aef0505c64b557494253c6c4db 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -99,8 +99,11 @@ let is_well_formed _s = p_true
let source = "Empty Model"
let load _sigma _obj () = Warning.error ~source "Can not load value in Empty model"
+let load_init _sigma _obj () = Warning.error ~source "Can not load init in Empty model"
let copied _s _obj () () = []
+let copied_init _s _obj () () = []
let stored _s _obj () _ = []
+let stored_init _s _obj () _ = []
let assigned _s _obj _sloc = []
let no_pointer () = Warning.error ~source "Can not compare pointers in Empty model"
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index f3c129e00646eae99fa6f829d360c8066caeeb39..982ecd1a45a26f259ca3486a7e2f826007d6688f 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -84,7 +84,7 @@ sig
val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
- val monotonic_init : Sigma.t -> Sigma.t -> pred
+ (* val monotonic_init : Sigma.t -> Sigma.t -> pred *)
end
@@ -115,8 +115,6 @@ struct
let pp_rid fmt r = if r <> 0 then Format.fprintf fmt "_R%03d" r
- let loadrec = ref (fun _ _ _ -> assert false)
-
(* -------------------------------------------------------------------------- *)
(* --- Frame Lemmas for Compound Access --- *)
(* -------------------------------------------------------------------------- *)
@@ -166,6 +164,84 @@ struct
) chunks
end
+ (* -------------------------------------------------------------------------- *)
+ (* --- Loader utils --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ module AKEY =
+ struct
+ type t = int * base * Matrix.t
+ and base = I of c_int | F of c_float | P | C of compinfo
+ let make r elt ds =
+ let base = match elt with
+ | C_int i -> I i
+ | C_float f -> F f
+ | C_pointer _ -> P
+ | C_comp c -> C c
+ | C_array _ -> raise (Invalid_argument "Wp.EqArray")
+ in r, base , ds
+ let key = function
+ | I i -> Ctypes.i_name i
+ | F f -> Ctypes.f_name f
+ | P -> "ptr"
+ | C c -> Lang.comp_id c
+ let key_init = function
+ | (I _ | F _ | P) as b -> key b ^ "_init"
+ | C c -> Lang.comp_init_id c
+ let obj = function
+ | I i -> C_int i
+ | F f -> C_float f
+ | P -> C_pointer Cil.voidPtrType
+ | C c -> C_comp c
+ let tau = function
+ | I _ -> Lang.t_int
+ | F f -> Lang.t_float f
+ | P -> Lang.t_addr ()
+ | C c -> Lang.t_comp c
+ let tau_init = function
+ | I _ | F _ | P -> Lang.t_bool
+ | C c -> Lang.t_init c
+ let compare (r,a,p) (s,b,q) =
+ if r = s then
+ let cmp = String.compare (key a) (key b) in
+ if cmp <> 0 then cmp else Matrix.compare p q
+ else r - s
+ let pretty fmt (r,a,ds) =
+ Format.fprintf fmt "%s%a%a" (key a) pp_rid r Matrix.pp_suffix_id ds
+ end
+
+ module type LOAD_INFO = sig
+ val kind : Lang.datakind
+ val footprint : c_object -> M.loc -> M.Sigma.domain
+ val t_comp : compinfo -> Lang.tau
+ val t_array : AKEY.base -> Lang.tau
+ val comp_id : compinfo -> string
+ val array_id : AKEY.base -> string
+ val load : M.Sigma.t -> c_object -> M.loc -> term
+ end
+
+ module VALUE_LOAD_INFO = struct
+ let kind = KValue
+ let footprint = M.value_footprint
+ let t_comp = Lang.t_comp
+ let t_array = AKEY.tau
+ let comp_id = Lang.comp_id
+ let array_id = AKEY.key
+ let load_rec = ref (fun _ _ _ -> assert false)
+ let load sigma = !load_rec sigma
+ end
+
+ module INIT_LOAD_INFO = struct
+ let kind = KInit
+ let footprint = M.init_footprint
+ let t_comp = Lang.t_init
+ let t_array = AKEY.tau_init
+ let comp_id = Lang.comp_init_id
+ let array_id = AKEY.key_init
+ let load_rec = ref (fun _ _ _ -> assert false)
+ let load sigma = !load_rec sigma
+ end
+
(* -------------------------------------------------------------------------- *)
(* --- Compound Loader --- *)
(* -------------------------------------------------------------------------- *)
@@ -177,9 +253,9 @@ struct
let pretty fmt (r,c) = Format.fprintf fmt "%d:%a" r Compinfo.pretty c
end
- module COMP = WpContext.Generator(COMP_KEY)
+ module COMP_GEN (Info : LOAD_INFO) = WpContext.Generator(COMP_KEY)
(struct
- let name = M.name ^ ".COMP"
+ let name = M.name ^ ".COMP" ^ (if Info.kind = KInit then "INIT" else "")
type key = int * compinfo
type data = lfun * chunk list
@@ -188,10 +264,10 @@ struct
let v = e_var x in
let obj = C_comp c in
let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
- let domain = M.value_footprint obj loc in
- let result = Lang.t_comp c in
+ let domain = Info.footprint obj loc in
+ let result = Info.t_comp c in
let lfun =
- Lang.generated_f ~result "Load%a_%s" pp_rid r (Lang.comp_id c)
+ Lang.generated_f ~result "Load%a_%s" pp_rid r (Info.comp_id c)
in
(* Since its a generated it is the unique name given *)
let xms,chunks,sigma = signature domain in
@@ -201,8 +277,8 @@ struct
| Some fields ->
let def = List.map
(fun f ->
- Cfield (f, KValue) ,
- !loadrec sigma (object_of f.ftype) (M.field loc f)
+ Cfield (f, Info.kind) ,
+ Info.load sigma (object_of f.ftype) (M.field loc f)
) fields
in
Definitions.Function( result , Def , e_record def )
@@ -219,50 +295,17 @@ struct
let compile = Lang.local generate
end)
+ module COMP = COMP_GEN(VALUE_LOAD_INFO)
+ module COMP_INIT = COMP_GEN(INIT_LOAD_INFO)
+
(* -------------------------------------------------------------------------- *)
(* --- Array Loader --- *)
(* -------------------------------------------------------------------------- *)
- module AKEY =
- struct
- type t = int * base * Matrix.t
- and base = I of c_int | F of c_float | P | C of compinfo
- let make r elt ds =
- let base = match elt with
- | C_int i -> I i
- | C_float f -> F f
- | C_pointer _ -> P
- | C_comp c -> C c
- | C_array _ -> raise (Invalid_argument "Wp.EqArray")
- in r, base , ds
- let key = function
- | I i -> Ctypes.i_name i
- | F f -> Ctypes.f_name f
- | P -> "ptr"
- | C c -> Lang.comp_id c
- let obj = function
- | I i -> C_int i
- | F f -> C_float f
- | P -> C_pointer Cil.voidPtrType
- | C c -> C_comp c
- let tau = function
- | I _ -> Lang.t_int
- | F f -> Lang.t_float f
- | P -> Lang.t_addr ()
- | C c -> Lang.t_comp c
- let compare (r,a,p) (s,b,q) =
- if r = s then
- let cmp = String.compare (key a) (key b) in
- if cmp <> 0 then cmp else Matrix.compare p q
- else r - s
- let pretty fmt (r,a,ds) =
- Format.fprintf fmt "%s%a%a" (key a) pp_rid r Matrix.pp_suffix_id ds
- end
-
- module ARRAY = WpContext.Generator(AKEY)
+ module ARRAY_GEN(Info: LOAD_INFO) = WpContext.Generator(AKEY)
(struct
open Matrix
- let name = M.name ^ ".ARRAY"
+ let name = M.name ^ ".ARRAY" ^ (if Info.kind=KInit then "INIT" else "")
type key = AKEY.t
type data = lfun * chunk list
@@ -271,11 +314,11 @@ struct
let v = e_var x in
let obj = AKEY.obj a in
let loc = M.of_region_pointer r obj v in (* t_pointer -> loc *)
- let domain = M.value_footprint obj loc in
- let result = Matrix.cc_tau (AKEY.tau a) ds in
+ let domain = Info.footprint obj loc in
+ let result = Matrix.cc_tau (Info.t_array a) ds in
let lfun =
Lang.generated_f ~result "Array%a_%s%a"
- pp_rid r (AKEY.key a) Matrix.pp_suffix_id ds in
+ pp_rid r (Info.array_id a) Matrix.pp_suffix_id ds in
let prefix = Lang.Fun.debug lfun in
let name = prefix ^ "_access" in
let xmem,chunks,sigma = signature domain in
@@ -283,7 +326,7 @@ struct
let phi = e_fun lfun (v :: env.size_val @ List.map e_var xmem) in
let va = List.fold_left e_get phi env.index_val in
let ofs = e_sum env.index_offset in
- let vm = !loadrec sigma obj (M.shift loc obj ofs) in
+ let vm = Info.load sigma obj (M.shift loc obj ofs) in
let lemma = p_hyps env.index_range (p_equal va vm) in
let cluster = cluster () in
Definitions.define_symbol {
@@ -310,29 +353,58 @@ struct
let compile = Lang.local generate
end)
+ module ARRAY = ARRAY_GEN(VALUE_LOAD_INFO)
+ module ARRAY_INIT = ARRAY_GEN(INIT_LOAD_INFO)
+
(* -------------------------------------------------------------------------- *)
- (* --- Loader --- *)
+ (* --- Loaders --- *)
(* -------------------------------------------------------------------------- *)
- let load_comp sigma comp loc =
- let r , p = M.to_region_pointer loc in
- let f , m = COMP.get (r,comp) in
- F.e_fun f (p :: memories sigma m)
+ module LOADER_GEN
+ (ATOM: sig
+ val load_int : M.Sigma.t -> c_int -> M.loc -> term
+ val load_float : M.Sigma.t -> c_float -> M.loc -> term
+ val load_pointer : M.Sigma.t -> typ -> M.loc -> term
+ end)
+ (COMP: sig val get : (int*compinfo) -> (lfun * chunk list) end)
+ (ARRAY: sig val get : (int*AKEY.base*Matrix.t) -> (lfun * chunk list) end)
+ = struct
+ let load_comp sigma comp loc =
+ let r , p = M.to_region_pointer loc in
+ let f , m = COMP.get (r,comp) in
+ F.e_fun f (p :: memories sigma m)
+
+ let load_array sigma a loc =
+ let r , p = M.to_region_pointer loc in
+ let e , ns = Ctypes.array_dimensions a in
+ let ds = Matrix.of_dims ns in
+ let f , m = ARRAY.get @@ AKEY.make r e ds in
+ F.e_fun f (p :: Matrix.cc_dims ns @ memories sigma m)
+
+ let load sigma obj loc =
+ match obj with
+ | C_int i -> ATOM.load_int sigma i loc
+ | C_float f -> ATOM.load_float sigma f loc
+ | C_pointer t -> ATOM.load_pointer sigma t loc
+ | C_comp c -> load_comp sigma c loc
+ | C_array a -> load_array sigma a loc
+ end
- let load_array sigma a loc =
- let r , p = M.to_region_pointer loc in
- let e , ns = Ctypes.array_dimensions a in
- let ds = Matrix.of_dims ns in
- let f , m = ARRAY.get @@ AKEY.make r e ds in
- F.e_fun f (p :: Matrix.cc_dims ns @ memories sigma m)
+ module VALUE_LOADER =
+ LOADER_GEN
+ (struct
+ let load_int = M.load_int
+ let load_float = M.load_float
+ let load_pointer sigma t loc =
+ snd @@ M.to_region_pointer @@ M.load_pointer sigma t loc
+ end)
+ (COMP)(ARRAY)
- let loadvalue sigma obj loc =
- match obj with
- | C_int i -> M.load_int sigma i loc
- | C_float f -> M.load_float sigma f loc
- | C_pointer t -> snd @@ M.to_region_pointer @@ M.load_pointer sigma t loc
- | C_comp c -> load_comp sigma c loc
- | C_array a -> load_array sigma a loc
+ let load_comp = VALUE_LOADER.load_comp
+ let load_array = VALUE_LOADER.load_array
+ let load_value = VALUE_LOADER.load
+
+ let () = VALUE_LOAD_INFO.load_rec := load_value
let load sigma obj loc =
let open Sigs in
@@ -343,8 +415,6 @@ struct
| C_comp c -> Val (load_comp sigma c loc)
| C_array a -> Val (load_array sigma a loc)
- let () = loadrec := loadvalue
-
(* -------------------------------------------------------------------------- *)
(* --- Initialized --- *)
(* -------------------------------------------------------------------------- *)
@@ -484,6 +554,17 @@ struct
"Invalid infinite range @[<hov 2>+@,(%a@,..%a)@]"
Vset.pp_bound low Vset.pp_bound up
+ module INIT_LOADER =
+ LOADER_GEN
+ (struct
+ let load_int sigma _ = M.is_init_atom sigma
+ let load_float sigma _ = M.is_init_atom sigma
+ let load_pointer sigma _ = M.is_init_atom sigma
+ end)(COMP_INIT)(ARRAY_INIT)
+
+ let load_init = INIT_LOADER.load
+ let () = INIT_LOAD_INFO.load_rec := load_init
+
(* -------------------------------------------------------------------------- *)
(* --- Havocs --- *)
(* -------------------------------------------------------------------------- *)
@@ -506,7 +587,7 @@ struct
let havoc_init_length = gen_havoc_length M.init_footprint
let havoc_init seq obj loc = havoc_init_length seq obj loc F.e_one
-
+(*
let set_init_length s obj loc length =
let ps = ref [] in
Domain.iter
@@ -518,14 +599,13 @@ struct
) (M.init_footprint obj loc) ; !ps
let set_init seq obj loc = set_init_length seq obj loc F.e_one
-
+*)
(* -------------------------------------------------------------------------- *)
(* --- Stored & Copied --- *)
(* -------------------------------------------------------------------------- *)
let updated_init_atom seq loc value =
- let new_value = e_or [M.is_init_atom seq.pre loc ; value ] in
- let chunk_init,mem_init = M.set_init_atom seq.pre loc new_value in
+ let chunk_init,mem_init = M.set_init_atom seq.pre loc value in
Set(Sigma.value seq.post chunk_init,mem_init)
let updated_atom seq obj loc value =
@@ -541,12 +621,20 @@ struct
let stored seq obj loc value =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- [ updated_atom seq obj loc value ; updated_init_atom seq loc e_true ]
+ [ updated_atom seq obj loc value ]
+ | C_comp _ | C_array _ ->
+ Set(load_value seq.post obj loc, value) :: havoc seq obj loc
+
+ let stored_init seq obj loc value =
+ match obj with
+ | C_int _ | C_float _ | C_pointer _ ->
+ [ updated_init_atom seq loc value ]
| C_comp _ | C_array _ ->
- let set_value = Set(loadvalue seq.post obj loc, value) in
- set_value :: havoc seq obj loc @ set_init seq obj loc
+ Set(load_init seq.post obj loc, value) :: havoc_init seq obj loc
+
+ let copied s obj p q = stored s obj p (load_value s.pre obj q)
- let copied s obj p q = stored s obj p (loadvalue s.pre obj q)
+ let copied_init s obj p q = stored_init s obj p (load_init s.pre obj q)
(* -------------------------------------------------------------------------- *)
(* --- Assigned --- *)
@@ -567,7 +655,7 @@ struct
havoc_init_length s obj (M.shift l obj a) (e_range a b)
let assigned seq obj sloc =
- Assert (M.monotonic_init seq.pre seq.post) ::
+ (* Assert (M.monotonic_init seq.pre seq.post) :: *)
match sloc with
| Sloc loc -> assigned_loc seq obj loc
| Sdescr(xs,loc,condition) ->
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index a9e1e89c9885214ca1410311f3f440a68a71bcb7..fdbdebffecf2042683303b435b3aff970bbe5dfa 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -80,7 +80,7 @@ sig
val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
- val monotonic_init : Sigma.t -> Sigma.t -> pred
+ (* val monotonic_init : Sigma.t -> Sigma.t -> pred *)
end
@@ -91,13 +91,16 @@ sig
val domain : c_object -> M.loc -> M.Sigma.domain
val load : M.Sigma.t -> c_object -> M.loc -> M.loc Sigs.value
- val loadvalue : M.Sigma.t -> c_object -> M.loc -> term
+ val load_init : M.Sigma.t -> c_object -> M.loc -> term
+ val load_value : M.Sigma.t -> c_object -> M.loc -> term
val havoc : M.Sigma.t sequence -> c_object -> M.loc -> equation list
val havoc_length : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
val stored : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
+ val stored_init : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
val copied : M.Sigma.t sequence -> c_object -> M.loc -> M.loc -> equation list
+ val copied_init : M.Sigma.t sequence -> c_object -> M.loc -> M.loc -> equation list
val assigned : M.Sigma.t sequence -> c_object -> M.loc sloc -> equation list
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 074692a5c4436985a790dd7d94dbcab7db1fc48d..e53e58af9be9a3735492aeeefcba76ed0faa6e54 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -827,10 +827,13 @@ end
module LOADER = MemLoader.Make(MODEL)
let load = LOADER.load
-let loadvalue = LOADER.loadvalue
+let load_init = LOADER.load_init
+let load_value = LOADER.load_value
let stored = LOADER.stored
+let stored_init = LOADER.stored_init
let copied = LOADER.copied
+let copied_init = LOADER.copied_init
let assigned = LOADER.assigned
let initialized = LOADER.initialized
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 939661b4ea3edd93b4a865af30e16476d7e2f3f8..abf67a6cb7c4af3ce67261a735ecfe22503268ff 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -579,7 +579,7 @@ module BASE = WpContext.Generator(Varinfo)
let initialization prefix x base =
match sizeof x with
- | Some size when x.vformal || x.vglob ->
+ | Some size when Cvalues.always_initialized x ->
let a = Lang.freshvar ~basename:"init" t_init in
let m = e_var a in
let init_access =
@@ -1075,23 +1075,30 @@ struct
let set_init obj loc ~length _chunk ~current =
let n = F.e_mul (length_of_object obj) length in
F.e_fun f_set_init [current;loc;n]
-
+(*
let monotonic_init s1 s2 =
let m1 = Sigma.value s1 T_init in
let m2 = Sigma.value s2 T_init in
F.p_call p_monotonic [m1; m2]
-
+*)
end
module LOADER = MemLoader.Make(MODEL)
let load = LOADER.load
+let load_init = LOADER.load_init
let stored = LOADER.stored
+let stored_init = LOADER.stored_init
let copied = LOADER.copied
-let assigned = LOADER.assigned
+let copied_init = LOADER.copied_init
let initialized = LOADER.initialized
let domain = LOADER.domain
+let assigned seq obj loc =
+ (* Maintain always initialized values initialized *)
+ Assert (p_call p_cinits [Sigma.value seq.post T_init]) ::
+ LOADER.assigned seq obj loc
+
(* -------------------------------------------------------------------------- *)
(* --- Loc Comparison --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 45cc5514fc77bf7cf02ef169a228cbabfc8f9311..f52667de01c571a2691cd026d23888b0e89aec09 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -780,36 +780,44 @@ struct
(fun l -> Loc l)
(M.load sigma.mem obj (mloc_of_path m x ofs))
+ let load_init sigma obj = function
+ | Ref _ ->
+ e_true
+ | Val((CREF|CVAL),x,_) when Cvalues.always_initialized x ->
+ Cvalues.initialized_obj obj
+ | Val((CREF|CVAL),x,ofs) ->
+ access_init (get_init_term sigma x) ofs
+ | Loc l ->
+ M.load_init sigma.mem obj l
+ | Val((CTXT _|CARR _|HEAP) as m,x,ofs) ->
+ M.load_init sigma.mem obj (mloc_of_path m x ofs)
+
(* -------------------------------------------------------------------------- *)
(* --- Memory Store --- *)
(* -------------------------------------------------------------------------- *)
- (* Note that this function purposely does not update init state *)
- let memvar_stored seq _obj l v =
- match l with
- | Ref x -> noref ~op:"write to" x
- | Val((CREF|CVAL),x,ofs) ->
- let v1 = get_term seq.pre x in
- let v2 = get_term seq.post x in
- Set( v2 , update v1 ofs v )
- | _ -> failwith "MemVar stored 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 memvar_stored kind seq x ofs v =
+ let get_term, update = match kind with
+ | KValue -> get_term, update
+ | KInit -> get_init_term, update_init
+ in
+ let v1 = get_term seq.pre x in
+ let v2 = get_term seq.post x in
+ Set( v2 , update v1 ofs v )
- let stored seq obj l v = match l with
+ let gen_stored kind seq obj l v =
+ let mstored = match kind with KValue -> M.stored | KInit -> M.stored_init in
+ match l with
| Ref x -> noref ~op:"write to" x
| 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)
+ [memvar_stored kind seq x ofs v]
| Val((CTXT _|CARR _|HEAP) as m,x,ofs) ->
- M.stored (mseq_of_seq seq) obj (mloc_of_path m x ofs) v
+ mstored (mseq_of_seq seq) obj (mloc_of_path m x ofs) v
| Loc l ->
- M.stored (mseq_of_seq seq) obj l v
+ mstored (mseq_of_seq seq) obj l v
+
+ let stored = gen_stored KValue
+ let stored_init = gen_stored KInit
let copied seq obj l1 l2 =
let v = match load seq.pre obj l2 with
@@ -817,6 +825,9 @@ struct
| Sigs.Loc l -> pointer_val l
in stored seq obj l1 v
+ let copied_init seq obj l1 l2 =
+ stored_init seq obj l1 (load_init seq.pre obj l2)
+
(* -------------------------------------------------------------------------- *)
(* --- Pointer Comparison --- *)
(* -------------------------------------------------------------------------- *)
@@ -1134,7 +1145,7 @@ struct
| Val(m,x,p) ->
if is_heap_allocated m then
M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
- else if (x.vformal || x.vglob) then
+ else if Cvalues.always_initialized x then
try valid_offset RW (vobject m x) p
with ShiftMismatch -> shift_mismatch l
else
@@ -1160,7 +1171,7 @@ struct
let p, a, b = normalize elt p in
let in_array = valid_range RW (vobject m x) p (elt, a, b) in
let initialized =
- if x.vformal || x.vglob then p_true
+ if Cvalues.always_initialized x then p_true
else initialized_range sigma (vobject m x) x p a b
in
F.p_imply (F.p_leq a b) (p_and in_array initialized)
@@ -1248,15 +1259,14 @@ struct
match scope with
| Leave -> []
| Enter ->
- let xs = List.filter
- (fun v -> is_mvar_alloc 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
+ let init_status v =
+ if v.vdefined || Cvalues.always_initialized v || not@@ is_mvar_alloc v
+ then None
+ else
+ let i = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in
+ Some (Lang.F.p_equal (access_init (get_init_term seq.post v) []) i)
in
- List.map uninitialized xs
+ List.filter_map init_status xs
let is_nullable m v =
let addr = nullable_address v in
@@ -1345,7 +1355,7 @@ struct
(*
let monotonic_initialized_genset s xs mem x ofs p =
- if x.vformal || x.vglob then [Assert p_true]
+ if always_init x then [Assert p_true]
else
let valid = valid_offset_path s.post Sigs.RW mem x ofs in
let a = get_init_term s.pre x in
@@ -1365,13 +1375,19 @@ struct
(* -------------------------------------------------------------------------- *)
let rec monotonic_initialized seq obj x ofs =
- if x.vformal || x.vglob then p_true
+ if Cvalues.always_initialized x then p_true
else
match obj with
+ (* Structure initialization is not monotonic *)
+ | C_comp _ -> p_true
+ (* Neither is initialization of arrays of structures *)
+ | C_array { arr_element=t } when Cil.isStructOrUnionType t -> p_true
+
| 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 ()
@@ -1385,35 +1401,20 @@ struct
let hyp = Vset.in_range (e_var v) low up in
let in_range = monotonic_initialized seq obj x ofs in
Lang.F.p_forall [v] (p_imply hyp in_range)
- | C_comp { cfields = None } ->
- p_imply
- (initialized_loc seq.pre obj x ofs)
- (initialized_loc seq.post obj x ofs)
- | C_comp { cfields = Some fields } ->
- 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 fields)
-
- 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_stored seq obj loc v) ::
- Assert(monotonic_initialized seq obj x ofs) ::
- (memvar_set_init seq x ofs init)
- | _ -> failwith "MemVar assigned on a non MemVar location"
let assigned_loc seq obj = function
| Ref x -> noref ~op:"assigns to" x
| Val((CVAL|CREF),x,[]) ->
[ Assert (monotonic_initialized seq obj x []) ]
- | Val((CVAL|CREF),_,_) as vloc ->
- let v = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
- memvar_assigned seq obj vloc (e_var v)
+ | Val((CVAL|CREF),x,ofs) ->
+ let value = Lang.freshvar ~basename:"v" (tau_of_object obj) in
+ memvar_stored KValue seq x ofs (e_var value) ::
+ if Cil.isStructOrUnionType x.vtype then []
+ else begin
+ let init = Lang.freshvar ~basename:"v" (init_of_object obj) in
+ Assert(monotonic_initialized seq obj x ofs) ::
+ [ memvar_stored KInit seq x ofs (e_var init) ]
+ end
| Val((HEAP|CTXT _|CARR _) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sloc (mloc_of_path m x ofs))
| Loc l ->
@@ -1423,19 +1424,18 @@ struct
match l with
| Ref x -> noref ~op:"assigns to" x
| Val((CVAL|CREF),x,[]) ->
- (* Note that 'obj' above corresponds to the elements *)
- let obj = Ctypes.object_of x.vtype in
- [ Assert (monotonic_initialized seq obj x []) ]
- | Val((CVAL|CREF),x,ofs) as vloc ->
- let te = Lang.tau_of_object elt in
- let v = Lang.freshvar ~basename:"v" Qed.Logic.(Array(Int,te)) in
- let rec get_obj obj = function
- | [] -> obj
- | Field(fi) :: l -> get_obj (Ctypes.object_of fi.ftype) l
- | Shift(obj, _) :: l -> get_obj obj l
- in
- let obj = get_obj (Ctypes.object_of x.vtype) ofs in
- memvar_assigned seq obj vloc (e_var v)
+ if Ctypes.is_compound elt then []
+ else
+ (* Note that 'obj' above corresponds to the elements *)
+ let obj = Ctypes.object_of x.vtype in
+ [ Assert (monotonic_initialized seq obj x []) ]
+
+ | Val((CVAL|CREF),x,ofs) ->
+ let f_array t =
+ e_var (Lang.freshvar ~basename:"v" Qed.Logic.(Array(Int, t))) in
+ [ memvar_stored KValue seq x ofs (f_array @@ Lang.tau_of_object elt) ;
+ memvar_stored KInit seq x ofs (f_array @@ Lang.init_of_object elt) ]
+
| Val((HEAP|CTXT _|CARR _) as m,x,ofs) ->
let l = mloc_of_path m x ofs in
M.assigned (mseq_of_seq seq) obj (Sarray(l,elt,n))
@@ -1610,8 +1610,7 @@ struct
match l with
| Ref x | Val((CVAL|CREF),x,_) ->
let init =
- if not (x.vformal || x.vglob) then [ Init x ]
- else []
+ if not @@ Cvalues.always_initialized x then [ Init x ] else []
in
Heap.Set.of_list ((Var x) :: init)
| Loc _ | Val((CTXT _|CARR _|HEAP),_,_) ->
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index d460cccd7f124c2c0840ec7db27d66ccd05d5677..4ba69ca09b78975e00476fbf2c4ac0285045700b 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -200,14 +200,20 @@ let set s m ks v = if ks = [] then v else update (e_var (Sigma.get s m)) ks v
let load sigma obj l =
if Ctypes.is_pointer obj then Loc (Star l) else Val(value sigma l)
+let load_init _sigma _obj _l = Warning.error ~source "Mem0Alias: No initialized"
+
let stored seq _obj l e =
let m,ks = access l in
let x = F.e_var (Sigma.get seq.post m) in
[Set( x , set seq.pre m ks e )]
+let stored_init _seq _obj _l _e = Warning.error ~source "Mem0Alias: No initialized"
+
let copied seq obj a b =
stored seq obj a (value seq.pre b)
+let copied_init _seq _obj _a _b = Warning.error ~source "Mem0Alias: No initialized"
+
let assigned _s _obj _sloc = []
type state = Chunk.t Tmap.t
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 9321b09c0dfc657f4a040baf4734fd5399dd69a5..83335aaf4119b97eb8924ec181f00f201c45c44b 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -422,6 +422,10 @@ sig
(** Return the value of the object of the given type at the given location in
the given memory state. *)
+ val load_init : sigma -> c_object -> loc -> term
+ (** Return the initialization status at the given location in the given
+ memory state. *)
+
val copied : sigma sequence -> c_object -> loc -> loc -> equation list
(**
Return a set of equations that express a copy between two memory state.
@@ -431,16 +435,36 @@ sig
[sigma.post] at [loc2].
*)
+ val copied_init : sigma sequence -> c_object -> loc -> loc -> equation list
+ (**
+ Return a set of equations that express a copy of an initialized state
+ between two memory state.
+
+ [copied sigma ty loc1 loc2] returns a set of formula expressing that the
+ initialization status for an object [ty] is the same in [sigma.pre] at
+ [loc1] and in [sigma.post] at [loc2].
+ *)
+
val stored : sigma sequence -> c_object -> loc -> term -> equation list
(**
Return a set of formula that express a modification between two memory
state.
- [copied sigma ty loc t] returns a set of formula expressing that
+ [stored sigma ty loc t] returns a set of formula expressing that
[sigma.pre] and [sigma.post] are identical except for an object [ty] at
location [loc] which is represented by [t] in [sigma.post].
*)
+ val stored_init : sigma sequence -> c_object -> loc -> term -> equation list
+ (**
+ Return a set of formula that express a modification of the initialization
+ status between two memory state.
+
+ [stored_init sigma ty loc t] returns a set of formula expressing that
+ [sigma.pre] and [sigma.post] are identical except for an object [ty] at
+ location [loc] which has a new init represented by [t] in [sigma.post].
+ *)
+
val assigned : sigma sequence -> c_object -> loc sloc -> equation list
(**
Return a set of formula that express that two memory state are the same
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index 07f1496d8129ab4cc3a91ab30906151be9a540d0..ba8d3245e87db470fa5b710e25c811b79803fa4e 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -700,12 +700,18 @@ struct
if Cil.isVolatileLval lv &&
Cvalues.volatile ~warn:"unsafe write-access to volatile l-value" ()
then None
- else Some
- begin
- match expr.enode with
- | Lval lv -> M.copied seq obj loc (C.lval seq.pre lv)
- | _ -> M.stored seq obj loc (C.val_of_exp seq.pre expr)
- end
+ else
+ let value = match expr.enode with
+ | Lval lv -> M.copied seq obj loc (C.lval seq.pre lv)
+ | _ -> M.stored seq obj loc (C.val_of_exp seq.pre expr)
+ in
+ let init = match expr.enode with
+ | Lval lv when Cil.(isStructOrUnionType @@ typeOfLval lv) ->
+ M.copied_init seq obj loc (C.lval seq.pre lv)
+ | _ ->
+ M.stored_init seq obj loc (Cvalues.initialized_obj obj)
+ in
+ Some (value @ init)
let assign wenv stmt lv expr wp = in_wenv wenv wp
begin fun env wp ->
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index 234959f116a6401da5586a53f15da7d2bf6d312d..f17512e54ed3ab79e74e472efda4e84a80800dee 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -240,7 +240,7 @@ one_assign sequent:
Assume {
Have: foo_0 = 42.
Have: (Init_d_0=false) /\ (ta_d_0=true) /\ (ta_d_1=false).
- Have: (Init_d_1=true) /\ (d = c).
+ Have: d = c.
}
Prove: d = c.
@@ -268,17 +268,11 @@ some_seq sequent:
Assume {
Have: foo_0 = 42.
Have: (Init_d_0=false) /\ (ta_d_0=true) /\ (ta_d_1=false).
- Have: (Init_d_1=true) /\ (d_1 = 0).
+ Have: d_1 = 0.
If c != 0
- Then {
- Have: ((Init_d_1=true) <-> (Init_d_2=true)) /\ (d_1 = d_2).
- Have: (Init_d_3=true) /\ (d = 1).
- }
+ Then { Have: d_1 = d_2. Have: d = 1. }
If c = 0
- Then {
- Have: ((Init_d_1=true) <-> (Init_d_4=true)) /\ (d_1 = d_3).
- Have: (Init_d_5=true) /\ (d = 2).
- }
+ Then { Have: d_1 = d_3. Have: d = 2. }
Have: ((c != 0) -> (d = 1)).
}
Prove: ((c = 0) -> (d = 2)).
@@ -292,17 +286,11 @@ some_seq sequent:
Assume {
Have: foo_0 = 42.
Have: (Init_d_0=false) /\ (ta_d_0=true) /\ (ta_d_1=false).
- Have: (Init_d_1=true) /\ (d_1 = 0).
+ Have: d_1 = 0.
If c != 0
- Then {
- Have: ((Init_d_1=true) <-> (Init_d_2=true)) /\ (d_1 = d_2).
- Have: (Init_d_3=true) /\ (d = 1).
- }
+ Then { Have: d_1 = d_2. Have: d = 1. }
If c = 0
- Then {
- Have: ((Init_d_1=true) <-> (Init_d_4=true)) /\ (d_1 = d_3).
- Have: (Init_d_5=true) /\ (d = 2).
- }
+ Then { Have: d_1 = d_3. Have: d = 2. }
}
Prove: ((c != 0) -> (d = 1)).
@@ -407,7 +395,7 @@ zloop sequent:
Have: 0 <= x.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
- Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
+ Have: (1 + i_1) = i_2.
Have: i_2 <= 10.
Have: i <= 10.
Have: 10 <= i.
@@ -429,7 +417,7 @@ zloop sequent:
Have: 0 <= x.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i = 0).
- Have: (Init_i_1=true) /\ ((1 + i) = i_1).
+ Have: (1 + i) = i_1.
Have: i_1 <= 10.
Have: i_2 <= 10.
Have: 10 <= i_2.
@@ -448,7 +436,7 @@ zloop sequent:
Have: 0 <= x.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
- Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
+ Have: (1 + i_1) = i_2.
Have: i_2 <= 10.
Have: i <= 10.
Have: 10 <= i.
@@ -466,7 +454,7 @@ zloop sequent:
Have: 0 <= x.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
- Have: (Init_i_1=true) /\ ((1 + i_1) = i).
+ Have: (1 + i_1) = i.
}
Prove: i <= 10.
@@ -481,12 +469,12 @@ zloop sequent:
Have: 0 <= x.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
- Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
+ Have: (1 + i_1) = i_2.
Have: i_2 <= 10.
Have: i_3 <= 10.
Have: i_3 <= 9.
- Have: (Init_i_2=true) /\ ((1 + i_3) = i_4).
- Have: (Init_i_3=true) /\ ((1 + i_4) = i).
+ Have: (1 + i_3) = i_4.
+ Have: (1 + i_4) = i.
}
Prove: i <= 10.
@@ -501,7 +489,7 @@ zloop sequent:
Have: 0 <= x.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i = 0).
- Have: (Init_i_1=true) /\ ((1 + i) = i_1).
+ Have: (1 + i) = i_1.
Have: i_1 <= 10.
Have: i_2 <= 10.
Have: 10 <= i_2.
@@ -685,49 +673,33 @@ compare sequent:
((b = a) /\ (a <= b) /\ (d <= c) /\
((b != a) \/ ((b = a) /\ (d <= c))))
If b < a
- Then {
- Have: ((Init_r_0=true) <-> (Init_r_1=true)) /\ (r_1 = r_2).
- Have: (Init_r_2=true) /\ (r = (-1)).
- }
+ Then { Have: r_1 = r_2. Have: r = (-1). }
If a <= b
Then {
- Have: ((Init_r_0=true) <-> (Init_r_3=true)) /\ (r_1 = r_3).
+ Have: r_1 = r_3.
If (b != a) \/ ((b = a) /\ (d <= c))
Then {
If b = a
Then {
- Have: ((Init_r_4=true) <-> (Init_r_5=true)) /\ (r_4 = r_5).
+ Have: r_4 = r_5.
If d <= c
- Then {
- Have: ((Init_r_5=true) <-> (Init_r_6=true)) /\ (r_5 = r_6).
- Have: (Init_r_7=true) /\ (r = 0).
- }
+ Then { Have: r_5 = r_6. Have: r = 0. }
If c < d
- Then {
- Have: ((Init_r_5=true) <-> (Init_r_8=true)) /\ (r_5 = r_7).
- Have: (Init_r_9=true) /\ (r = 1).
- }
+ Then { Have: r_5 = r_7. Have: r = 1. }
}
If b != a
- Then {
- Have: ((Init_r_4=true) <-> (Init_r_10=true)) /\ (r_4 = r_8).
- Have: (Init_r_11=true) /\ (r = 1).
- }
+ Then { Have: r_4 = r_8. Have: r = 1. }
}
If b = a
Then {
- Have: ((Init_r_3=true) <-> (Init_r_12=true)) /\ (r_3 = r_9).
+ Have: r_3 = r_9.
If c < d
- Then {
- Have: ((Init_r_12=true) <-> (Init_r_13=true)) /\ (r_9 = r_10).
- Have: (Init_r_14=true) /\ (r = (-1)).
- }
+ Then { Have: r_9 = r_10. Have: r = (-1). }
If d <= c
- Then { Have: ((Init_r_12=true) <-> (Init_r_4=true)) /\ (r_9 = r_4).
- }
+ Then { Have: r_9 = r_4. }
}
If b != a
- Then { Have: ((Init_r_3=true) <-> (Init_r_4=true)) /\ (r_3 = r_4). }
+ Then { Have: r_3 = r_4. }
}
}
Prove: ((a < b) -> (r = 1)).
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
index 85e1744ce2042bb31ce0c09fb458e8a778278825..471e631c00131d0e3f2b0bd358d4efd9871b475d 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test_rela.res.oracle
@@ -23,10 +23,7 @@ Sequent: Assume {
Then { Have: (node_0=true). }
(* Set: tmp = c *)
If (node_3=true)
- Then {
- Have: (Init_tmp_0=true) /\ (tmp_0 = c_2).
- Have: (node_2=true).
- }
+ Then { Have: tmp_0 = c_2. Have: (node_2=true). }
(* Set: c = c + 100 *)
If (node_4=true)
Then { Have: (100 + c_3) = c_2. Have: (node_3=true). }
@@ -42,7 +39,7 @@ Sequent: Assume {
(* Entering scope [tmp]: effect: (not Init_tmp_0) /\ (not ta_tmp_0) /\ ta_tmp_1 *)
If (node_9=true)
Then {
- Have: (Init_tmp_1=false) /\ (ta_tmp_1=true) /\ (ta_tmp_2=false).
+ Have: (Init_tmp_0=false) /\ (ta_tmp_1=true) /\ (ta_tmp_2=false).
Have: (node_6=true).
}
If (node_7=true)
@@ -62,10 +59,7 @@ Sequent: Assume {
Then { Have: (node_10=true). }
(* Set: tmp = c *)
If (node_13=true)
- Then {
- Have: (Init_tmp_2=true) /\ (tmp_1 = c_5).
- Have: (node_12=true).
- }
+ Then { Have: tmp_1 = c_5. Have: (node_12=true). }
(* Set: c = c + 100 *)
If (node_14=true)
Then { Have: (100 + c_6) = c_5. Have: (node_13=true). }
@@ -78,10 +72,10 @@ Sequent: Assume {
Then { Have: (node_17=true). }
Else { Have: (node_18=true). }
}
- (* Entering scope [tmp]: effect: (not Init_tmp_4) /\ (not ta_tmp_6) /\ ta_tmp_7 *)
+ (* Entering scope [tmp]: effect: (not Init_tmp_3) /\ (not ta_tmp_6) /\ ta_tmp_7 *)
If (node_19=true)
Then {
- Have: (Init_tmp_3=false) /\ (ta_tmp_4=true) /\ (ta_tmp_5=false).
+ Have: (Init_tmp_1=false) /\ (ta_tmp_4=true) /\ (ta_tmp_5=false).
Have: (node_16=true).
}
If (node_17=true)
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
index aa706417403927b3103953f705ae7129155d96e3..174f0ba544e6f7d5cd22d98d0a91afc8618d955f 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memtyped.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -wp-prop=CHECK
+ OPT: -wp-prop=CHECK,FAILS
*/
/* run.config_qualif
- OPT: -wp-prop=CHECK
+ OPT: -wp-prop=CHECK,FAILS
*/
struct S {
@@ -33,7 +33,7 @@ void range(struct S* s){
for(int i = 0; i < 10; ++i){
if(1 <= i && i <= 4) s->a[i] = 1 ;
}
- //@ check CHECK: \initialized(s);
+ //@ check FAILS: \initialized(s); // memtyped assigns not monotonic
}
void field(struct S* s){
@@ -48,7 +48,7 @@ void field(struct S* s){
for(int i = 0; i < 10; ++i){
s->i++;
}
- //@ check CHECK: \initialized(s);
+ //@ check FAILS: \initialized(s); // memtyped assigns not monotonic
}
void array(struct S* s){
@@ -66,7 +66,7 @@ void array(struct S* s){
for(int i = 0; i < 10; ++i){
s->a[i] = 1 ;
}
- //@ check CHECK: \initialized(s);
+ //@ check FAILS: \initialized(s); // memtyped assigns not monotonic
}
void index(struct S* s){
@@ -81,7 +81,7 @@ void index(struct S* s){
for(int i = 0; i < 10; ++i){
if(i == 4) s->a[i] = 1 ;
}
- //@ check CHECK: \initialized(s);
+ //@ check FAILS: \initialized(s); // memtyped assigns not monotonic
}
void descr(struct S* s){
@@ -96,7 +96,7 @@ void descr(struct S* s){
for(int i = 0; i < 10; ++i){
if(i == 0 || i == 2 || i == 4) s->a[i] = 1 ;
}
- //@ check CHECK: \initialized(s);
+ //@ check FAILS: \initialized(s); // memtyped assigns not monotonic
}
void comp(struct S* s){
@@ -115,7 +115,7 @@ void comp(struct S* s){
s->a[i] = 1 ;
s->i++;
}
- //@ check CHECK: \initialized(s);
+ //@ check FAILS: \initialized(s); // memtyped assigns not monotonic
}
struct S glob ;
@@ -123,7 +123,7 @@ struct S * pg = &glob ;
struct S * const cg = &glob ;
void assigned_glob(void){
- //@ check CHECK: \initialized(cg);
+ //@ check FAILS: \initialized(cg); // no default init for structs
pg->i = 0;
/*@
loop invariant CHECK: 0 <= i <= 10 && \initialized(&pg->a[0 .. i-1]);
@@ -139,6 +139,6 @@ void assigned_glob(void){
pg->a[i] = 1 ;
pg->i++;
}
- //@ check CHECK: \initialized(pg);
- //@ check CHECK: \initialized(cg);
+ //@ check FAILS: \initialized(pg); // memtyped assigns not monotonic
+ //@ check FAILS: \initialized(cg); // no default init for structs
}
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
index 7fc06531a4a98bdc28c75c9bf07b40e0dd9a1f33..869eff6a1b7f6cd18dce59aa2f9d702dfb98fed6 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_initialized_memvar.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -wp-prop=CHECK
+ OPT: -wp-prop=CHECK,FAILS
*/
/* run.config_qualif
- OPT: -wp-prop=CHECK -wp-timeout 20
+ OPT: -wp-prop=CHECK,FAILS -wp-timeout 20
*/
struct S {
@@ -54,7 +54,7 @@ void field(void){
for(int i = 0; i < 10; ++i){
s.i++;
}
- //@ check CHECK: \initialized(&s);
+ //@ check FAILS: \initialized(&s); // initialization not monotonic
}
void array(void){
@@ -73,7 +73,7 @@ void array(void){
for(int i = 0; i < 10; ++i){
s.a[i] = 1 ;
}
- //@ check CHECK: \initialized(&s);
+ //@ check FAILS: \initialized(&s); // initialization not monotonic
}
void index(void){
@@ -89,7 +89,7 @@ void index(void){
for(int i = 0; i < 10; ++i){
if(i == 4) s.a[i] = 1 ;
}
- //@ check CHECK: \initialized(&s);
+ //@ check FAILS: \initialized(&s); // initialization not monotonic
}
void descr(void){
@@ -128,5 +128,5 @@ void comp(void){
s.a[i] = 1 ;
s.i++;
}
- //@ check CHECK: \initialized(&s);
+ //@ check FAILS: \initialized(&s); // initialization not monotonic
}
diff --git a/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i
index 6c9a2d5554a89a7ceb890d3c51adff2ea0f9b1f2..c132688581846299ab3e92a82b701644c3bc0ea1 100644
--- a/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/assigned_not_initialized_memtyped.i
@@ -47,7 +47,7 @@ void assigned_glob_comp(void){
/*@ loop assigns i, *pg_comp, *cg_comp; */
for(int i = 0; i < 10; ++i){}
//@ check FAIL: \initialized(pg_comp);
- //@ check OK: \initialized(cg_comp);
+ //@ check FAIL: \initialized(cg_comp); // struct not initialized by default
}
int glob_array[10] ;
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memvar.i b/src/plugins/wp/tests/wp_acsl/initialized_memvar.i
index a5b3f6a265e111e5d5fa3571dc9667371d4c532a..ce1b1d8f09207f96d73fedb09db3f8ccd1af06b5 100644
--- a/src/plugins/wp/tests/wp_acsl/initialized_memvar.i
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memvar.i
@@ -13,7 +13,7 @@ int a[10] ;
struct C c ;
struct C ac [10];
-
+//@ requires \initialized(&c) && \initialized(&ac);
void globals(void){
// Simple type
//@ check qed_ok: \initialized(&x) ;
@@ -32,10 +32,10 @@ void globals(void){
//@ check qed_ok: \initialized(&c.s) ;
//@ check qed_ok: \initialized(&c.s.y) ;
- //@ check qed_ok: \initialized(&c.a) ;
- //@ check qed_ok: \initialized(&c.a[4]) ;
- //@ check qed_ko: \initialized(&c.a[10]) ;
- //@ check qed_ok: \initialized(&c.a[0 .. 9]) ;
+ //@ check provable: \initialized(&c.a) ;
+ //@ check provable: \initialized(&c.a[4]) ;
+ //@ check not_provable: \initialized(&c.a[10]) ;
+ //@ check provable: \initialized(&c.a[0 .. 9]) ;
//@ check qed_ko: \initialized(&c.a[0 .. 10]) ;
// Complex accesses
diff --git a/src/plugins/wp/tests/wp_acsl/opaque_struct.i b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
index 208ef8612069f9516f4c82afe5911ebecf5ea455..c1e457182f2950047598a6d1005b47d07461e5da 100644
--- a/src/plugins/wp/tests/wp_acsl/opaque_struct.i
+++ b/src/plugins/wp/tests/wp_acsl/opaque_struct.i
@@ -23,14 +23,14 @@ struct S* p ;
//@ assigns *p ;
void g(void);
-/*@ requires \initialized(p);
+/*@ requires \initialized(p);
requires \valid(p);
*/
void initialized_assigns(void){
g();
- //@ check succeed: \initialized(p);
+ //@ check fails: \initialized(p); // struct initialization not monotonic
//@ check succeed: \block_length(p) >= 0;
-
+
// while it can be proved in Coq, this is currently
// too indirect for solvers.
// @ check succeed: \block_length(p) >= \block_length(&S1);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
index 97405e3f05094dc1e00ff8b5ea4a0116d4336bc0..eb064ee4a7ea78989f9b37536d5b006fced95df1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memtyped.res.oracle
@@ -6,32 +6,32 @@
Function array
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 69):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 69):
Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a = shiftfield_F1_S_a(s).
Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Init_undef_1, m, a_1, 10).
-Let a_3 = havoc(Init_undef_0, m, a_1, 10).
+Let a_2 = havoc(Init_undef_0, m, a_1, 10).
+Let a_3 = havoc(Init_undef_1, m, a_1, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(m, a_2).
+ Have: cinits(a_3).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a, i_2)]=true)))).
+ (a_3[shift_sint32(a, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_2, a_3).
+ Have: cinits(a_2).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
-Prove: IsInit_S1_S(s, a_3).
+Prove: IsInit_S1_S(s, a_2).
------------------------------------------------------------
@@ -55,22 +55,22 @@ Prove: true.
Function assigned_glob
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 126):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 126):
Assume { (* Heap *) Type: cinits(Init_0). }
Prove: IsInit_S1_S(global(G_glob_82), Init_0).
------------------------------------------------------------
Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 129):
-Let m = Init_0[shiftfield_F1_S_i(pg_0) <- true].
Let a = shiftfield_F1_S_a(pg_0).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(pg_0) <- true],
+ shift_sint32(a, 0), 10).
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Heap *)
Type: (region(pg_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_1).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
@@ -89,59 +89,59 @@ Prove: true.
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 142):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 142):
Let m = Init_0[shiftfield_F1_S_i(pg_0) <- true].
-Let a = shiftfield_F1_S_a(pg_0).
-Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, m, pg_0, 11).
+Let a = havoc(Init_undef_0, m, pg_0, 11).
+Let a_1 = shiftfield_F1_S_a(pg_0).
+Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(pg_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_2).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ (a_2[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_1, a_2).
+ Have: cinits(a).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
-Prove: IsInit_S1_S(pg_0, a_2).
+Prove: IsInit_S1_S(pg_0, a).
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 143):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 143):
Let m = Init_0[shiftfield_F1_S_i(pg_0) <- true].
-Let a = shiftfield_F1_S_a(pg_0).
-Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, m, pg_0, 11).
+Let a = havoc(Init_undef_0, m, pg_0, 11).
+Let a_1 = shiftfield_F1_S_a(pg_0).
+Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(pg_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_2).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ (a_2[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_1, a_2).
+ Have: cinits(a).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
-Prove: IsInit_S1_S(global(G_glob_82), a_2).
+Prove: IsInit_S1_S(global(G_glob_82), a).
------------------------------------------------------------
@@ -197,31 +197,31 @@ Prove: (-1) <= i.
Function comp
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 118):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 118):
Let m = Init_0[shiftfield_F1_S_i(s) <- true].
-Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
-Let a_2 = havoc(Init_undef_0, m, s, 11).
+Let a = havoc(Init_undef_0, m, s, 11).
+Let a_1 = shiftfield_F1_S_a(s).
+Let a_2 = havoc(Init_undef_1, m, shift_sint32(a_1, 0), 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_2).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ (a_2[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_1, a_2).
+ Have: cinits(a).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
-Prove: IsInit_S1_S(s, a_2).
+Prove: IsInit_S1_S(s, a).
------------------------------------------------------------
@@ -260,34 +260,33 @@ Prove: (-1) <= i.
Function descr
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 99):
-Let a = shiftfield_F1_S_i(s).
-Let m = Init_1[a <- true].
-Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = shift_sint32(a_1, 0).
-Let a_3 = havoc(Init_undef_0, m, a_2, 10).
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 99):
+Let a = shiftfield_F1_S_a(s).
+Let a_1 = shiftfield_F1_S_i(s).
+Let a_2 = shift_sint32(a, 0).
+Let a_3 = havoc(Init_undef_0, Init_1[a_1 <- true], a_2, 10).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_1).
(* Loop assigns ... *)
- Have: monotonic_init(m, a_3).
+ Have: cinits(a_3).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_3[shift_sint32(a_1, i_2)]=true)))).
+ (a_3[shift_sint32(a, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_3, Init_0) /\
+ Have: cinits(Init_0) /\
(forall a_4 : addr.
((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
- (shift_sint32(a_1, i_2) != a_4))) ->
+ (shift_sint32(a, i_2) != a_4))) ->
((a_3[a_4]=true) <-> (Init_0[a_4]=true)))) /\
(forall a_4 : addr.
((forall i_2 : Z. (((i_2 = 0) \/ (i_2 = 2) \/ (i_2 = 4)) ->
- (shift_sint32(a_1, i_2) != a_4))) ->
- (havoc(Mint_undef_0, Mint_0[a <- 0], a_2, 10)[a_4] = Mint_1[a_4]))).
+ (shift_sint32(a, i_2) != a_4))) ->
+ (havoc(Mint_undef_0, Mint_0[a_1 <- 0], a_2, 10)[a_4] = Mint_1[a_4]))).
(* Else *)
Have: 10 <= i_1.
}
@@ -350,28 +349,27 @@ Prove: true.
Function field
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 51):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 51):
Let a = shiftfield_F1_S_i(s).
-Let m = Init_0[a <- true].
Let a_1 = shiftfield_F1_S_a(s).
-Let a_2 = havoc(Init_undef_0, m, shift_sint32(a_1, 0), 10).
-Let a_3 = a_2[a <- true].
+Let a_2 = havoc(Init_undef_0, Init_0[a <- true], shift_sint32(a_1, 0), 10).
+Let a_3 = a_2[a <- i].
Assume {
- Type: is_sint32(i) /\ is_sint32(i_1).
+ Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(m, a_2).
+ Have: cinits(a_2).
(* Invariant *)
- Have: (0 <= i) /\ (i <= 10) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
- (a_2[shift_sint32(a_1, i_2)]=true)))).
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
+ (a_2[shift_sint32(a_1, i_3)]=true)))).
(* Else *)
- Have: 10 <= i.
+ Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_2, a_3).
+ Have: cinits(a_3).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i_2.
}
Prove: IsInit_S1_S(s, a_3).
@@ -391,18 +389,17 @@ Prove: true.
Function index
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 84):
-Let m = Init_0[shiftfield_F1_S_i(s) <- true].
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 84):
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
-Let a_2 = shift_sint32(a, 4).
-Let a_3 = a_1[a_2 <- i | Init_undef_0[a_2]].
+Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(s) <- true],
+ shift_sint32(a, 0), 10).
+Let a_2 = a_1[shift_sint32(a, 4) <- i].
Assume {
Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_1).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
@@ -410,11 +407,11 @@ Assume {
(* Else *)
Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_1, a_3).
+ Have: cinits(a_2).
(* Else *)
Have: 10 <= i_2.
}
-Prove: IsInit_S1_S(s, a_3).
+Prove: IsInit_S1_S(s, a_2).
------------------------------------------------------------
@@ -439,15 +436,15 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 16):
-Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(s) <- true],
+ shift_sint32(a, 0), 10).
Assume {
Type: is_sint32(i) /\ is_sint32(1 + i).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_1).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
@@ -467,15 +464,15 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 21):
-Let m = Init_0[shiftfield_F1_S_i(s) <- true].
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_0, m, shift_sint32(a, 0), 10).
+Let a_1 = havoc(Init_undef_0, Init_0[shiftfield_F1_S_i(s) <- true],
+ shift_sint32(a, 0), 10).
Assume {
Type: is_sint32(i).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_1).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
@@ -507,17 +504,17 @@ Prove: true.
Function range
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 36):
-Let m = Init_0[shiftfield_F1_S_i(s) <- true].
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 36):
Let a = shiftfield_F1_S_a(s).
-Let a_1 = havoc(Init_undef_1, m, shift_sint32(a, 0), 10).
+Let a_1 = havoc(Init_undef_1, Init_0[shiftfield_F1_S_i(s) <- true],
+ shift_sint32(a, 0), 10).
Let a_2 = havoc(Init_undef_0, a_1, shift_sint32(a, 1), 4).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(m, a_1).
+ Have: cinits(a_1).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
@@ -525,7 +522,7 @@ Assume {
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: monotonic_init(a_1, a_2).
+ Have: cinits(a_2).
(* Else *)
Have: 10 <= i_1.
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
index 846c03241554a4f8ac8844069c0832abe60d4d8b..4de0de53912a6e0648a9b3c96317d751d6de734d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_initialized_memvar.res.oracle
@@ -6,7 +6,7 @@
Function array
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 76):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memvar.i, line 76):
Assume {
Have: 0 <= i.
Have: i <= 9.
@@ -17,9 +17,6 @@ Assume {
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v_1[i_3]=true)))))).
(* Else *)
Have: 10 <= i_1.
- (* Loop assigns 'CHECK' *)
- Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v_1[i_3]=true) ->
- (v[i_3]=true)))).
(* Invariant *)
Have: (0 <= i_2) /\ (i_2 <= 10).
(* Else *)
@@ -37,28 +34,23 @@ Prove: true.
Function comp
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 131):
-Let a = Init_s_0.Init_F1_S_a.
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memvar.i, line 131):
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
- (* Loop assigns 'CHECK' *)
- Have: ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v[i_3]=true) ->
- (a[i_3]=true))))).
+ Have: 10 <= i.
(* Invariant *)
- Have: (0 <= i_2) /\ (i_2 <= 10).
+ Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
@@ -195,21 +187,21 @@ Prove: true.
Function field
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 57):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memvar.i, line 57):
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (v[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
@@ -221,23 +213,21 @@ Prove: true.
Function index
------------------------------------------------------------
-Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 92):
+Goal Check 'FAILS' (file tests/wp_acsl/assigned_initialized_memvar.i, line 92):
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
- (* Loop assigns 'CHECK' *)
- Have: ((v[4]=true) -> (v_1=true)).
+ Have: 10 <= i.
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (v[4 <- v_1][i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
index 89ab8bf1720a2de09a8da18b3acf6a838fbb223b..c9c0e0bd12771fce0e8d415916c972f67912aba7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigned_not_initialized_memtyped.res.oracle
@@ -13,7 +13,7 @@ Assume {
(* Heap *)
Type: (region(array_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, a).
+ Have: cinits(a).
(* Else *)
Have: 10 <= i.
}
@@ -33,7 +33,7 @@ Assume {
(* Heap *)
Type: (region(pg_array_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, a) /\ monotonic_init(a, a_1).
+ Have: cinits(a) /\ cinits(a_1).
(* Else *)
Have: 10 <= i.
}
@@ -50,7 +50,7 @@ Assume {
(* Heap *)
Type: (region(pg_array_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, a_1) /\ monotonic_init(a_1, a_2).
+ Have: cinits(a_1) /\ cinits(a_2).
(* Else *)
Have: 10 <= i.
}
@@ -62,33 +62,21 @@ Prove: IsInitArray_sint32(a, 10, a_2).
------------------------------------------------------------
Goal Check 'FAIL' (file tests/wp_acsl/assigned_not_initialized_memtyped.i, line 38):
-Let a = global(G_glob_atomic_39).
-Let m = Init_0[a <- i_1 | Init_0[a]].
-Let P = m[pg_atomic_0].
-Assume {
- Type: is_sint32(i_2).
- (* Heap *)
- Type: (region(pg_atomic_0.base) <= 0) /\ cinits(Init_0).
- (* Loop assigns ... *)
- Have: monotonic_init(Init_0, m) /\
- monotonic_init(m, m[pg_atomic_0 <- i | P]).
- (* Else *)
- Have: 10 <= i_2.
-}
-Prove: (i=true) \/ (P=true).
+Assume { Type: is_sint32(i_1). (* Else *) Have: 10 <= i_1. }
+Prove: (i=true).
------------------------------------------------------------
Goal Check 'OK' (file tests/wp_acsl/assigned_not_initialized_memtyped.i, line 39):
Let a = global(G_glob_atomic_39).
-Let m = Init_0[a <- i | Init_0[a]].
-Let m_1 = m[pg_atomic_0 <- i_1 | m[pg_atomic_0]].
+Let m = Init_0[a <- i].
+Let m_1 = m[pg_atomic_0 <- i_1].
Assume {
Type: is_sint32(i_2).
(* Heap *)
Type: (region(pg_atomic_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, m) /\ monotonic_init(m, m_1).
+ Have: cinits(m) /\ cinits(m_1).
(* Else *)
Have: 10 <= i_2.
}
@@ -107,7 +95,7 @@ Assume {
(* Heap *)
Type: (region(pg_comp_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, a) /\ monotonic_init(a, a_1).
+ Have: cinits(a) /\ cinits(a_1).
(* Else *)
Have: 10 <= i.
}
@@ -115,7 +103,7 @@ Prove: IsInit_S1_S(pg_comp_0, a_1).
------------------------------------------------------------
-Goal Check 'OK' (file tests/wp_acsl/assigned_not_initialized_memtyped.i, line 50):
+Goal Check 'FAIL' (file tests/wp_acsl/assigned_not_initialized_memtyped.i, line 50):
Let a = global(G_glob_comp_45).
Let a_1 = havoc(Init_undef_1, Init_0, a, 11).
Let a_2 = havoc(Init_undef_0, a_1, pg_comp_0, 11).
@@ -124,7 +112,7 @@ Assume {
(* Heap *)
Type: (region(pg_comp_0.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, a_1) /\ monotonic_init(a_1, a_2).
+ Have: cinits(a_1) /\ cinits(a_2).
(* Else *)
Have: 10 <= i.
}
@@ -136,17 +124,8 @@ Prove: IsInit_S1_S(a, a_2).
------------------------------------------------------------
Goal Check 'FAIL' (file tests/wp_acsl/assigned_not_initialized_memtyped.i, line 16):
-Let P = Init_0[ptr_0].
-Assume {
- Type: is_sint32(i_1).
- (* Heap *)
- Type: (region(ptr_0.base) <= 0) /\ cinits(Init_0).
- (* Loop assigns ... *)
- Have: monotonic_init(Init_0, Init_0[ptr_0 <- i | P]).
- (* Else *)
- Have: 10 <= i_1.
-}
-Prove: (i=true) \/ (P=true).
+Assume { Type: is_sint32(i_1). (* Else *) Have: 10 <= i_1. }
+Prove: (i=true).
------------------------------------------------------------
------------------------------------------------------------
@@ -160,7 +139,7 @@ Assume {
(* Heap *)
Type: (region(s.base) <= 0) /\ cinits(Init_0).
(* Loop assigns ... *)
- Have: monotonic_init(Init_0, a).
+ Have: cinits(a).
(* Else *)
Have: 10 <= i.
}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
index 5a91bd928d651804096c4ff7df91b8872952db8d..efbea9e28a276a4a63ed90fc0d6c47346d8389cc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memvar.res.oracle
@@ -51,23 +51,59 @@ Prove: true.
------------------------------------------------------------
-Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 35):
-Prove: true.
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 35):
+Let a = Init_c_0.Init_F2_C_s.
+Let a_1 = Init_c_0.Init_F2_C_a.
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 9).
+ (* Pre-condition *)
+ Have: ((Init_c_0.Init_F2_C_x)=true) /\ ((a.Init_F1_S_x)=true) /\
+ ((a.Init_F1_S_y)=true) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) -> (a_1[i_1]=true)))).
+}
+Prove: (a_1[i]=true).
------------------------------------------------------------
-Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 36):
-Prove: true.
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 36):
+Let a = Init_c_0.Init_F2_C_s.
+Let a_1 = Init_c_0.Init_F2_C_a.
+Assume {
+ (* Pre-condition *)
+ Have: ((Init_c_0.Init_F2_C_x)=true) /\ ((a.Init_F1_S_x)=true) /\
+ ((a.Init_F1_S_y)=true) /\
+ (forall i : Z. ((0 <= i) -> ((i <= 9) -> (a_1[i]=true)))).
+}
+Prove: (a_1[4]=true).
------------------------------------------------------------
-Goal Check 'qed_ko' (file tests/wp_acsl/initialized_memvar.i, line 37):
-Prove: false.
+Goal Check 'not_provable' (file tests/wp_acsl/initialized_memvar.i, line 37):
+Let a = Init_c_0.Init_F2_C_s.
+Let a_1 = Init_c_0.Init_F2_C_a.
+Assume {
+ (* Pre-condition *)
+ Have: ((Init_c_0.Init_F2_C_x)=true) /\ ((a.Init_F1_S_x)=true) /\
+ ((a.Init_F1_S_y)=true) /\
+ (forall i : Z. ((0 <= i) -> ((i <= 9) -> (a_1[i]=true)))).
+}
+Prove: (a_1[10]=true).
------------------------------------------------------------
-Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memvar.i, line 38):
-Prove: true.
+Goal Check 'provable' (file tests/wp_acsl/initialized_memvar.i, line 38):
+Let a = Init_c_0.Init_F2_C_s.
+Let a_1 = Init_c_0.Init_F2_C_a.
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 9).
+ (* Pre-condition *)
+ Have: ((Init_c_0.Init_F2_C_x)=true) /\ ((a.Init_F1_S_x)=true) /\
+ ((a.Init_F1_S_y)=true) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 9) -> (a_1[i_1]=true)))).
+}
+Prove: (a_1[i]=true).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index d4c7697396c0754d0efbf5e6a48a36d31a20260f..519985dbf06721b87bb7f9823c5b53859268672c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
@@ -108,7 +108,7 @@ Prove: a_1 = x.
Function initialized_assigns
------------------------------------------------------------
-Goal Check 'succeed' (file tests/wp_acsl/opaque_struct.i, line 31):
+Goal Check 'fails' (file tests/wp_acsl/opaque_struct.i, line 31):
Let a = havoc(Init_undef_0, Init_0, p, Length_of_S1_S).
Assume {
(* Heap *)
@@ -118,7 +118,7 @@ Assume {
(* Pre-condition *)
Have: valid_rw(Malloc_0, p, Length_of_S1_S).
(* Call Effects *)
- Have: monotonic_init(Init_0, a).
+ Have: cinits(a).
}
Prove: IsInit_S1_S(p, a).
@@ -147,7 +147,7 @@ Assume {
(* Pre-condition *)
Have: !IsInit_S1_S(p, Init_0).
(* Call Effects *)
- Have: monotonic_init(Init_0, a).
+ Have: cinits(a).
}
Prove: !IsInit_S1_S(p, a).
@@ -161,7 +161,7 @@ Assume {
(* Pre-condition *)
Have: !IsInit_S1_S(p, Init_0).
(* Call Effects *)
- Have: monotonic_init(Init_0, a).
+ Have: cinits(a).
}
Prove: IsInit_S1_S(p, a).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 083f7d0ff4956ba090210e61d5f4da2817ea3822..f0921bf043d45d9f26e8b56579084bd06212bc5e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -4,9 +4,9 @@
[rte] annotating function foo
[wp] 2 goals scheduled
---------------------------------------------
---- Context 'typed_foo' Cluster 'Chunk'
+--- Context 'typed_foo' Cluster 'Init_S1_X'
---------------------------------------------
-theory Chunk
+theory Init_S1_X
(* use why3.BuiltIn.BuiltIn *)
(* use bool.Bool *)
@@ -21,18 +21,8 @@ theory Chunk
(* use map.Map *)
- (* use frama_c_wp.memory.Memory *)
-
- (* use frama_c_wp.cint.Cint *)
-
- predicate is_sint8_chunk (m:addr -> int) =
- forall a:addr. is_sint8 (get m a)
-
- predicate is_sint16_chunk (m:addr -> int) =
- forall a:addr. is_sint16 (get m a)
-
- predicate is_sint32_chunk (m:addr -> int) =
- forall a:addr. is_sint32 (get m a)
+ type Init_S1_X =
+ | Init_S1_X1 (Init_F1_X_a:bool) (Init_F1_X_b:bool) (Init_F1_X_c:bool)
end
---------------------------------------------
--- Context 'typed_foo' Cluster 'S1_X'
@@ -93,6 +83,12 @@ theory Compound
S1_X1 (get mchar (shiftfield_F1_X_a p)) (get mint (shiftfield_F1_X_b p))
(get mint1 (shiftfield_F1_X_c p))
+ (* use Init_S1_X *)
+
+ function Load_Init_S1_X (p:addr) (init:addr -> bool) : Init_S1_X =
+ Init_S1_X1 (get init (shiftfield_F1_X_a p))
+ (get init (shiftfield_F1_X_b p)) (get init (shiftfield_F1_X_c p))
+
Q_Load_S1_X_update_Mchar0 :
forall mchar:addr -> int, mint:addr -> int, mint1:addr -> int, p:addr, q:
addr, v:int [Load_S1_X p (set mchar q v) mint mint1].
@@ -161,6 +157,56 @@ theory Compound
separated p 3 q n ->
Load_S1_X p mchar mint (havoc mint2 mint1 q n)
= Load_S1_X p mchar mint mint1
+
+ Q_Load_Init_S1_X_update_Init0 :
+ forall init:addr -> bool, p:addr, q:addr, v:bool
+ [Load_Init_S1_X p (set init q v)].
+ separated p 3 q 1 ->
+ Load_Init_S1_X p (set init q v) = Load_Init_S1_X p init
+
+ Q_Load_Init_S1_X_eqmem_Init0 :
+ forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
+ [Load_Init_S1_X p init, eqmem init init1 q n| Load_Init_S1_X p init1,
+ eqmem init init1 q n].
+ included p 3 q n ->
+ eqmem init init1 q n -> Load_Init_S1_X p init1 = Load_Init_S1_X p init
+
+ Q_Load_Init_S1_X_havoc_Init0 :
+ forall init:addr -> bool, init1:addr -> bool, n:int, p:addr, q:addr
+ [Load_Init_S1_X p (havoc init1 init q n)].
+ separated p 3 q n ->
+ Load_Init_S1_X p (havoc init1 init q n) = Load_Init_S1_X p init
+end
+---------------------------------------------
+--- Context 'typed_foo' Cluster 'Chunk'
+---------------------------------------------
+theory Chunk
+ (* use why3.BuiltIn.BuiltIn *)
+
+ (* use bool.Bool *)
+
+ (* use int.Int *)
+
+ (* use int.ComputerDivision *)
+
+ (* use real.RealInfix *)
+
+ (* use frama_c_wp.qed.Qed *)
+
+ (* use map.Map *)
+
+ (* use frama_c_wp.memory.Memory *)
+
+ (* use frama_c_wp.cint.Cint *)
+
+ predicate is_sint8_chunk (m:addr -> int) =
+ forall a:addr. is_sint8 (get m a)
+
+ predicate is_sint16_chunk (m:addr -> int) =
+ forall a:addr. is_sint16 (get m a)
+
+ predicate is_sint32_chunk (m:addr -> int) =
+ forall a:addr. is_sint32 (get m a)
end
[wp:print-generated]
theory WP
@@ -180,15 +226,16 @@ end
(* use frama_c_wp.memory.Memory *)
- (* use Chunk *)
-
- (* use S1_X *)
+ (* use Init_S1_X *)
(* use Compound *)
+ (* use Chunk *)
+
goal wp_goal :
- forall t:addr -> bool, t1:int -> int, t2:addr -> int, t3:addr -> int, t4:
- addr -> int, a:addr.
+ forall t:addr -> bool, x:Init_S1_X, t1:int -> int, t2:addr -> int, t3:
+ addr -> int, t4:addr -> int, a:addr.
+ Load_Init_S1_X a t = x ->
region (base a) <= 0 ->
is_sint16_chunk t3 ->
is_sint32_chunk t4 ->
@@ -273,6 +320,8 @@ Assume {
(* Assertion 'rte,mem_access' *)
Have: valid_rd(Malloc_0, p, 3).
(* Initializer *)
+ Init: Load_Init_S1_X(p, Init_0) = Init_r_0.
+ (* Initializer *)
Init: a = r.
}
Prove: valid_rw(Malloc_0, p, 3).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
index 660872093ac27a7d2ae67acedee77f2b66c6c471..db28901d4032a8c3cce0c255267c3c9c147c1a84 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.res.oracle
@@ -9,53 +9,53 @@
[wp] [Qed] Goal typed_initialize_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_range_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_field_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_field_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_field_loop_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_array_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_array_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_array_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_index_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_descr_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_comp_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_comp_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_comp_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_comp_loop_assigns_part3 : Valid
-[wp] [Alt-Ergo] Goal typed_assigned_glob_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_assigned_glob_check_FAILS : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_glob_loop_invariant_CHECK_preserved : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_invariant_CHECK_established : Valid
-[wp] [Alt-Ergo] Goal typed_assigned_glob_check_CHECK_2 : Valid
-[wp] [Alt-Ergo] Goal typed_assigned_glob_check_CHECK_3 : Valid
+[wp] [Alt-Ergo] Goal typed_assigned_glob_check_FAILS_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_assigned_glob_check_FAILS_3 : Unsuccess
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part1 : Valid
[wp] [Qed] Goal typed_assigned_glob_loop_assigns_2_part2 : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_loop_assigns_2_part3 : Valid
-[wp] Proved goals: 42 / 42
+[wp] Proved goals: 33 / 42
Qed: 27
- Alt-Ergo: 15
+ Alt-Ergo: 6 (unsuccess: 9)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 4 2 6 100%
- range 3 1 4 100%
- field 2 1 3 100%
- array 3 1 4 100%
- index 3 1 4 100%
- descr 4 2 6 100%
- comp 2 2 4 100%
- assigned_glob 6 5 11 100%
+ range 3 - 4 75.0%
+ field 2 - 3 66.7%
+ array 3 - 4 75.0%
+ index 3 - 4 75.0%
+ descr 4 1 6 83.3%
+ comp 2 1 4 75.0%
+ assigned_glob 6 2 11 72.7%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
index 756f8f52f89bb4a6eef18e377b0eb803cb2f6922..a6ac6e2e3e5b69d98057d2bbdbcadea97f288094 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.res.oracle
@@ -12,11 +12,11 @@
[wp] [Qed] Goal typed_range_check_CHECK : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_field_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_field_loop_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_array_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_array_loop_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_index_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_invariant_CHECK_preserved : Valid
@@ -27,18 +27,18 @@
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part4 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_comp_check_FAILS : Unsuccess
[wp] [Qed] Goal typed_comp_loop_assigns : Valid
-[wp] Proved goals: 26 / 26
+[wp] Proved goals: 22 / 26
Qed: 15
- Alt-Ergo: 11
+ Alt-Ergo: 7 (unsuccess: 4)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
range 3 2 5 100%
- field 1 1 2 100%
- array 1 1 2 100%
- index 2 1 3 100%
+ field 1 - 2 50.0%
+ array 1 - 2 50.0%
+ index 2 - 3 66.7%
descr 5 3 8 100%
- comp 1 1 2 100%
+ comp 1 - 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
index 183c0c59b683a4e8f1257724c2d6ea67dbd8ef8a..86af5a8a55da89d485a5a2480c5c24a241f1a067 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_not_initialized_memtyped.res.oracle
@@ -9,18 +9,18 @@
[wp] [Alt-Ergo] Goal typed_assigned_glob_atomic_check_FAIL : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_glob_atomic_check_OK : Valid
[wp] [Alt-Ergo] Goal typed_assigned_glob_comp_check_FAIL : Unsuccess
-[wp] [Alt-Ergo] Goal typed_assigned_glob_comp_check_OK : Valid
+[wp] [Alt-Ergo] Goal typed_assigned_glob_comp_check_FAIL_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_glob_array_check_FAIL : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_glob_array_check_OK : Valid
-[wp] Proved goals: 3 / 9
+[wp] Proved goals: 2 / 9
Qed: 0
- Alt-Ergo: 3 (unsuccess: 6)
+ Alt-Ergo: 2 (unsuccess: 7)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
atomic - - 1 0.0%
comp - - 1 0.0%
array - - 1 0.0%
assigned_glob_atomic - 1 2 50.0%
- assigned_glob_comp - 1 2 50.0%
+ assigned_glob_comp - - 2 0.0%
assigned_glob_array - 1 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
index fa2acc12292c85ee69c240a5795f611dfc93f72f..245eaec165028cc5c3486c8cb5ef6cf5cc1942f6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.res.oracle
@@ -12,28 +12,28 @@
[wp] [Qed] Goal typed_globals_check_qed_ok_5 : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_6 : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_7 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_2 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_not_provable : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_3 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_3 : Unsuccess
[wp] [Qed] Goal typed_globals_check_qed_ok_8 : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_9 : Valid
-[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_3 : Unsuccess
[wp] [Qed] Goal typed_globals_check_qed_ok_10 : Valid
-[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_4 : Unsuccess
[wp] [Qed] Goal typed_globals_check_qed_ok_11 : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_12 : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_13 : Valid
-[wp] [Qed] Goal typed_globals_check_qed_ok_14 : Valid
-[wp] [Qed] Goal typed_globals_check_qed_ok_15 : Valid
-[wp] [Qed] Goal typed_globals_check_qed_ok_16 : Valid
-[wp] [Alt-Ergo] Goal typed_globals_check_provable : Valid
-[wp] [Alt-Ergo] Goal typed_globals_check_provable_2 : Valid
-[wp] [Alt-Ergo] Goal typed_globals_check_provable_3 : Valid
[wp] [Alt-Ergo] Goal typed_globals_check_provable_4 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_5 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_6 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_provable_7 : Valid
+[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_4 : Unsuccess
[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_5 : Unsuccess
[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_6 : Unsuccess
[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_7 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_8 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_globals_check_not_provable : Unsuccess
[wp] [Alt-Ergo] Goal typed_globals_check_not_provable_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_globals_check_not_provable_3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_globals_check_not_provable_4 : Unsuccess
[wp] [Qed] Goal typed_locals_check_qed_ok : Valid
[wp] [Qed] Goal typed_locals_check_qed_ok_2 : Valid
[wp] [Qed] Goal typed_locals_check_qed_ok_3 : Valid
@@ -58,10 +58,10 @@
[wp] [Qed] Goal typed_locals_check_qed_ok_20 : Valid
[wp] [Qed] Goal typed_locals_check_qed_ok_21 : Valid
[wp] Proved goals: 43 / 54
- Qed: 37
- Alt-Ergo: 6 (unsuccess: 11)
+ Qed: 34
+ Alt-Ergo: 9 (unsuccess: 11)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- globals 16 4 31 64.5%
+ globals 13 7 31 64.5%
locals 21 2 23 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index d8a3007152e5b4197ca3f5e108cc6fb410023cd2..ffca345397b95ff7963379b5e563fc3f6d562997 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -8,24 +8,24 @@
[wp] [Alt-Ergo] Goal typed_check_lemma_succeed_L2 : Valid
[wp] [Alt-Ergo] Goal typed_assigns_check_fail : Unsuccess
[wp] [Qed] Goal typed_assigns_check_succeed : Valid
+[wp] [Alt-Ergo] Goal typed_initialized_assigns_check_fails : Unsuccess
[wp] [Alt-Ergo] Goal typed_initialized_assigns_check_succeed : Valid
-[wp] [Alt-Ergo] Goal typed_initialized_assigns_check_succeed_2 : Valid
[wp] [Alt-Ergo] Goal typed_uninitialized_assigns_check_fail : Unsuccess
[wp] [Alt-Ergo] Goal typed_uninitialized_assigns_check_fail_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigned_via_pointer_check_fail : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_fail_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_assigns_effect_check_succeed : Valid
-[wp] Proved goals: 6 / 13
+[wp] Proved goals: 5 / 13
Qed: 2
- Alt-Ergo: 4 (unsuccess: 7)
+ Alt-Ergo: 3 (unsuccess: 8)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic test 1 1 3 66.7%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
assigns 1 - 2 50.0%
- initialized_assigns - 2 2 100%
+ initialized_assigns - 1 2 50.0%
uninitialized_assigns - - 2 0.0%
assigned_via_pointer - - 1 0.0%
assigns_effect - 1 3 33.3%
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index e73a0f100136a788210f0f92688f6d7036d9ec5b..22ca444e6a537298516bfc57f628ad0aaa4ab32c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -434,11 +434,12 @@ Assume {
Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (0 <= i_4) /\ (i_1 <= i_4) /\ (i_5 <= 9) /\ (i_4 <= 19).
@@ -469,11 +470,12 @@ Assume {
Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (0 <= i_4) /\ (i_1 <= i_4) /\ (i_5 <= 9) /\ (i_4 <= 19).
@@ -711,10 +713,11 @@ Assume {
Have: 0 <= i.
Have: i <= 9.
(* Loop assigns 'tactic,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
@@ -743,10 +746,11 @@ Assume {
Have: 0 <= i.
Have: i <= 9.
(* Loop assigns 'tactic,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index 81badf95a29a8e16c113baa7ff30109199227ff9..e1a3e723628fe25622cc96dc7c7b8c5d6a5e0cfb 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -434,11 +434,12 @@ Assume {
Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (0 <= i_4) /\ (i_1 <= i_4) /\ (i_5 <= 9) /\ (i_4 <= 19).
@@ -469,11 +470,12 @@ Assume {
Have: i <= 9.
Have: i_1 <= 19.
(* Loop assigns 'lack,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
- ((i_4 <= 19) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((0 <= i_4) -> ((i_5 <= 9) ->
+ ((i_4 <= 19) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (0 <= i_4) /\ (i_1 <= i_4) /\ (i_5 <= 9) /\ (i_4 <= 19).
@@ -711,10 +713,11 @@ Assume {
Have: 0 <= i.
Have: i <= 9.
(* Loop assigns 'tactic,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
@@ -743,10 +746,11 @@ Assume {
Have: 0 <= i.
Have: i <= 9.
(* Loop assigns 'tactic,Zone' *)
- Have: forall a : addr.
- ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
- (Mint_0[a] = Mint_1[a])).
+ Have: cinits(Init_0) /\
+ (forall a : addr.
+ ((forall i_5,i_4 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (shift_sint32(shift_A20_sint32(global(G_t2_52), i_5), i_4) != a)))) ->
+ (Mint_0[a] = Mint_1[a]))).
}
Prove: exists i_5,i_4 : Z. (i_5 <= i) /\ (i_4 <= i_1) /\ (0 <= i_5) /\
(i <= i_5) /\ (i_1 <= i_4) /\ (i_5 <= 9).
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index 139c4b84bd1e576dc0599b4e37e84f80df85cf87..d6b2be2c19d0a3c9227fced20293f93102d3d5bc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0072,
- "steps": 22 } ],
+ "verdict": "valid", "time": 0.0109,
+ "steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0051,
- "steps": 22 } ] } } ]
+ "verdict": "valid", "time": 0.0114,
+ "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index 139c4b84bd1e576dc0599b4e37e84f80df85cf87..d6b2be2c19d0a3c9227fced20293f93102d3d5bc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E$i$i0$i$i9" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0072,
- "steps": 22 } ],
+ "verdict": "valid", "time": 0.0109,
+ "steps": 24 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0051,
- "steps": 22 } ] } } ]
+ "verdict": "valid", "time": 0.0114,
+ "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index 33766e0ffa284cf9e2dc32ec7068dc49f6ec3021..e5407bbcb4c8cf4efe72f5628e6a2a6edd6cdb67 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -23,6 +23,9 @@ Assume {
When: (0 <= i) /\ (i < n).
(* Pre-condition *)
Have: (0 <= n) /\ (n <= 3).
+ Have: ({ Init_p_0 with Init_F1_S_n = true }) = Init_p_0.
+ (* Loop assigns ... *)
+ Have: ({ Init_p_0 with Init_F1_S_a = v_1 }) = Init_p_0.
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
(Mint_0[shift_sint32(a, i_2)] = v[i_2]))).
@@ -40,9 +43,12 @@ Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
(* Pre-condition *)
Have: (0 <= n) /\ (n <= 3).
+ Have: ({ Init_p_0 with Init_F1_S_n = true }) = Init_p_0.
+ (* Loop assigns ... *)
+ Have: ({ Init_p_0 with Init_F1_S_a = v }) = Init_p_0.
(* Invariant *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (Mint_0[shift_sint32(global(G_b_26), i_1)] = v[i_1]))).
+ (Mint_0[shift_sint32(global(G_b_26), i_1)] = v_1[i_1]))).
(* Invariant *)
Have: (0 <= i) /\ (i <= n).
(* Then *)
@@ -65,6 +71,9 @@ Assume {
When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: (0 <= n) /\ (n <= 3).
+ Have: ({ Init_p_0 with Init_F1_S_n = true }) = Init_p_0.
+ (* Loop assigns ... *)
+ Have: ({ Init_p_0 with Init_F1_S_a = v_1 }) = Init_p_0.
(* Invariant *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(Mint_0[shift_sint32(a, i_2)] = v[i_2]))).