From e1a9e36a8caabd2f70ce8de64c3ca7610a600eef Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 7 May 2020 10:58:38 +0200
Subject: [PATCH] [wp] Improves MemLoader initialized
---
src/plugins/wp/MemLoader.ml | 243 +++++++++---------
src/plugins/wp/MemLoader.mli | 4 +-
src/plugins/wp/MemMemory.ml | 12 +-
src/plugins/wp/MemMemory.mli | 1 +
src/plugins/wp/MemRegion.ml | 4 +
src/plugins/wp/MemTyped.ml | 15 +-
.../wp/share/why3/frama_c_wp/memory.mlw | 18 +-
.../wp/tests/wp_acsl/initialized_memtyped.i | 8 +-
.../assigned_initialized_memtyped.res.oracle | 141 +++++-----
.../oracle/initialized_memtyped.res.oracle | 130 +++++-----
.../initialized_memtyped.res.oracle | 16 +-
11 files changed, 311 insertions(+), 281 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index f4ea3e2c086..be5fa8a2158 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -79,8 +79,10 @@ sig
val store_float : Sigma.t -> c_float -> loc -> term -> Chunk.t * term
val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
- val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val is_init_atom : Sigma.t -> loc -> term
+ 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
end
@@ -113,7 +115,6 @@ struct
let pp_rid fmt r = if r <> 0 then Format.fprintf fmt "_R%03d" r
let loadrec = ref (fun _ _ _ -> assert false)
- let initrec = ref (fun _ _ _ -> assert false)
(* -------------------------------------------------------------------------- *)
(* --- Frame Lemmas for Compound Access --- *)
@@ -175,18 +176,9 @@ struct
let pretty fmt (r,c) = Format.fprintf fmt "%d:%a" r Compinfo.pretty c
end
- module type COMP_CONFIG = sig
- val name: string
- val footprint: c_object -> M.loc -> M.Sigma.domain
- val tau_of: compinfo -> tau
- val id_of: compinfo -> string
- val kind: datakind
- val load: Sigma.t -> c_object -> M.loc -> term
- end
-
- module COMPGEN(C: COMP_CONFIG) = WpContext.Generator(COMP_KEY)
+ module COMP = WpContext.Generator(COMP_KEY)
(struct
- let name = M.name ^ "." ^ C.name
+ let name = M.name ^ ".COMP"
type key = int * compinfo
type data = lfun * chunk list
@@ -195,15 +187,17 @@ 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 = C.footprint obj loc in
- let result = C.tau_of c in
- let lfun = Lang.generated_f ~result "Load%a_%s" pp_rid r (C.id_of c) in
+ let domain = M.value_footprint obj loc in
+ let result = Lang.tau_of_comp c in
+ let lfun =
+ Lang.generated_f ~result "Load%a_%s" pp_rid r (Lang.comp_id c)
+ in
(* Since its a generated it is the unique name given *)
let xms,chunks,sigma = signature domain in
let def = List.map
(fun f ->
- Cfield (f, C.kind) ,
- C.load sigma (object_of f.ftype) (M.field loc f)
+ Cfield (f, KValue) ,
+ !loadrec sigma (object_of f.ftype) (M.field loc f)
) c.cfields in
let dfun = Definitions.Function( result , Def , e_record def ) in
Definitions.define_symbol {
@@ -218,25 +212,6 @@ struct
let compile = Lang.local generate
end)
- module COMP = COMPGEN
- (struct
- let name = "COMP"
- let footprint = M.value_footprint
- let tau_of = Lang.tau_of_comp
- let id_of = Lang.comp_id
- let kind = KValue
- let load sigma = !loadrec sigma
- end)
- module COMPINIT = COMPGEN
- (struct
- let name = "COMPINIT"
- let footprint = M.init_footprint
- let tau_of = Lang.init_of_comp
- let id_of = Lang.comp_init_id
- let kind = KInit
- let load sigma = !initrec sigma
- end)
-
(* -------------------------------------------------------------------------- *)
(* --- Array Loader --- *)
(* -------------------------------------------------------------------------- *)
@@ -250,18 +225,10 @@ struct
if r1 = r2 then Matrix.NATURAL.compare m1 m2 else r1-r2
end
- module type ARRAY_CONFIG = sig
- val name: string
- val footprint: c_object -> M.loc -> M.Sigma.domain
- val tau_of_matrix: c_object -> Matrix.dim list -> tau
- val fun_ext: string
- val load: Sigma.t -> c_object -> M.loc -> term
- end
-
- module ARRAYGEN(C: ARRAY_CONFIG) = WpContext.Generator(ARRAY_KEY)
+ module ARRAY = WpContext.Generator(ARRAY_KEY)
(struct
open Matrix
- let name = M.name ^ "." ^ C.name
+ let name = M.name ^ ".ARRAY"
type key = int * arrayinfo * Matrix.matrix
type data = lfun * chunk list
@@ -270,12 +237,11 @@ struct
let v = e_var x in
let obj_a = C_array ainfo in
let loc = M.of_region_pointer r obj_a v in (* t_pointer -> loc *)
- let domain = C.footprint obj_a loc in
- let result = C.tau_of_matrix obj_e ds in
+ let domain = M.value_footprint obj_a loc in
+ let result = Matrix.tau obj_e ds in
let lfun =
- Lang.generated_f ~result "Array%s%a%s_%s"
- C.fun_ext pp_rid r
- (Matrix.id ds) (Matrix.natural_id obj_e)
+ Lang.generated_f ~result "Array%a%s_%s"
+ pp_rid r (Matrix.id ds) (Matrix.natural_id obj_e)
in
let prefix = Lang.Fun.debug lfun in
let axiom = prefix ^ "_access" in
@@ -284,7 +250,7 @@ struct
let phi = e_fun lfun (v :: denv.size_val @ List.map e_var xmem) in
let va = List.fold_left e_get phi denv.index_val in
let ofs = e_sum denv.index_offset in
- let vm = C.load sigma obj_e (M.shift loc obj_e ofs) in
+ let vm = !loadrec sigma obj_e (M.shift loc obj_e ofs) in
let lemma = p_hyps denv.index_range (p_equal va vm) in
let cluster = cluster () in
Definitions.define_symbol {
@@ -311,25 +277,6 @@ struct
let compile = Lang.local generate
end)
- module ARRAY = ARRAYGEN
- (struct
- let name = "ARRAY"
- let footprint = M.value_footprint
- let tau_of_matrix = Matrix.tau
- let fun_ext = ""
- let load sigma = !loadrec sigma
- end)
-
- module ARRAYINIT = ARRAYGEN
- (struct
- let name = "ARRAYINIT"
- let footprint = M.init_footprint
- let tau_of_matrix = Matrix.init
- let fun_ext = "Init"
- let load sigma = !initrec sigma
- end)
-
-
(* -------------------------------------------------------------------------- *)
(* --- Loader --- *)
(* -------------------------------------------------------------------------- *)
@@ -368,52 +315,92 @@ struct
(* --- Initialized --- *)
(* -------------------------------------------------------------------------- *)
- let initvalue_comp sigma comp loc =
+ let isinitrec = ref (fun _ _ _ -> assert false)
+
+ module IS_INIT_COMP = WpContext.Generator(COMP_KEY)
+ (struct
+ let name = M.name ^ ".IS_INIT_COMP"
+ type key = int * compinfo
+ type data = lfun * chunk list
+
+ let generate (r,c) =
+ let x = Lang.freshvar ~basename:"p" (Lang.t_addr()) in
+ 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.init_footprint obj loc in
+ let name =
+ Format.asprintf "Is%s%a" (Lang.comp_init_id c) pp_rid r
+ in
+ let lfun = Lang.generated_p name in
+ let xms,chunks,sigma = signature domain in
+ let def = List.map
+ (fun f -> !isinitrec sigma (object_of f.ftype) (M.field loc f))
+ c.cfields
+ in
+ let dfun = Definitions.Predicate(Def , p_conj def ) in
+ Definitions.define_symbol {
+ d_lfun = lfun ; d_types = 0 ;
+ d_params = x :: xms ;
+ d_definition = dfun ;
+ d_cluster = cluster () ;
+ } ;
+ lfun , chunks
+
+ let compile = Lang.local generate
+ end)
+
+ module ARRAYINIT = WpContext.Generator(ARRAY_KEY)
+ (struct
+ open Matrix
+ let name = M.name ^ ".ARRAYINIT"
+ type key = int * arrayinfo * Matrix.matrix
+ type data = lfun * chunk list
+
+ let generate (r,ainfo,(obj_e,ds)) =
+ let x = Lang.freshvar ~basename:"p" (Lang.t_addr()) in
+ let v = e_var x in
+ let obj_a = C_array ainfo in
+ let loc = M.of_region_pointer r obj_a v in (* t_pointer -> loc *)
+ let domain = M.init_footprint obj_a loc in
+ let name = Format.asprintf "IsInitArray%a%s_%s"
+ pp_rid r (Matrix.id ds) (Matrix.natural_id obj_e)
+ in
+ let lfun = Lang.generated_p name in
+ let xmem,chunks,sigma = signature domain in
+ let denv = Matrix.denv ds in
+ let ofs = e_sum denv.index_offset in
+ let vm = !isinitrec sigma obj_e (M.shift loc obj_e ofs) in
+ let def = p_forall denv.index_var (p_hyps denv.index_range vm) in
+ Definitions.define_symbol {
+ d_lfun = lfun ; d_types = 0 ;
+ d_params = x :: denv.size_var @ xmem ;
+ d_definition = Predicate (Def, def) ;
+ d_cluster = cluster () ;
+ } ;
+ lfun , chunks
+
+ let compile = Lang.local generate
+ end)
+
+ let initialized_comp sigma comp loc =
let r , p = M.to_region_pointer loc in
- let f , m = COMPINIT.get (r,comp) in
- F.e_fun f (p :: memories sigma m)
+ let f , m = IS_INIT_COMP.get (r,comp) in
+ F.p_call f (p :: memories sigma m)
- let initvalue_array sigma a loc =
+ let initialized_array sigma a loc =
let d = Matrix.of_array a in
let r , p = M.to_region_pointer loc in
let f , m = ARRAYINIT.get (r,a,d) in
- F.e_fun f (p :: Matrix.size d @ memories sigma m)
+ F.p_call f (p :: Matrix.size d @ memories sigma m)
- let initvalue sigma obj loc =
+ let initialized_loc sigma obj loc =
match obj with
- | C_int _ | C_float _ | C_pointer _ -> M.is_init_atom sigma loc
- | C_comp ci -> initvalue_comp sigma ci loc
- | C_array a -> initvalue_array sigma a loc
-
- let () = initrec := initvalue
+ | C_int _ | C_float _ | C_pointer _ -> p_bool (M.is_init_atom sigma loc)
+ | C_comp ci -> initialized_comp sigma ci loc
+ | C_array a -> initialized_array sigma a loc
- let rec initialized_loc sigma obj loc =
- match obj with
- | C_int _ | C_float _ | C_pointer _ ->
- p_bool (initvalue sigma obj loc)
- | C_comp ci ->
- let initialized_field f =
- initialized_loc sigma (object_of f.ftype) (M.field loc f)
- in
- p_conj (List.map initialized_field ci.cfields)
- | C_array ai ->
- let obj_e, ds = Matrix.of_array ai in
- let denv = Matrix.denv ds in
- let access =
- List.fold_left
- (fun loc ofs -> M.shift loc obj_e ofs) loc denv.index_val
- in
- let make_subst var size p =
- match size with
- | None -> p
- | Some i -> p_subst_var var (e_int i) p
- in
- let substs = List.map2 make_subst denv.size_var ds in
- let conj =
- List.fold_left (fun p f -> f p) (p_conj denv.index_range) substs
- in
- p_forall denv.index_var
- (p_imply conj (initialized_loc sigma obj_e access))
+ let () = isinitrec := initialized_loc
let initialized sigma = function
| Rloc(obj, loc) -> initialized_loc sigma obj loc
@@ -432,7 +419,7 @@ struct
(* --- Havocs --- *)
(* -------------------------------------------------------------------------- *)
- let havoc_length s obj loc length =
+ let gen_havoc_length get_domain s obj loc length =
let ps = ref [] in
Domain.iter
(fun chunk ->
@@ -443,15 +430,31 @@ struct
let fresh = F.e_var (Lang.freshvar ~basename tau) in
let havoc = M.havoc obj loc ~length chunk ~fresh ~current:pre in
ps := Set(post,havoc) :: !ps
- ) (domain obj loc) ; !ps
+ ) (get_domain obj loc) ; !ps
+ let havoc_length = gen_havoc_length M.value_footprint
let havoc seq obj loc = havoc_length seq obj loc F.e_one
+ 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
+ (fun chunk ->
+ let pre = Sigma.value s.pre chunk in
+ let post = Sigma.value s.post chunk in
+ let set = M.set_init obj loc ~length chunk ~current:pre in
+ ps := Set(post,set) :: !ps
+ ) (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 seq loc value =
+ let updated_init_atom seq loc value =
let chunk_init,mem_init = M.set_init_atom seq.pre loc value in
Set(Sigma.value seq.post chunk_init,mem_init)
@@ -468,11 +471,10 @@ struct
let stored seq obj loc value =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- updated_init seq loc e_true :: [ updated_atom seq obj loc value ]
+ updated_atom seq obj loc value :: [ updated_init_atom seq loc e_true ]
| C_comp _ | C_array _ ->
- let init = Cvalues.initialized_obj obj in
- Set(initvalue seq.post obj loc, init) ::
- Set(loadvalue seq.post obj loc, value) :: havoc seq obj loc
+ let set_value = Set(loadvalue seq.post obj loc, value) in
+ set_value :: havoc seq obj loc @ set_init seq obj loc
let copied s obj p q = stored s obj p (loadvalue s.pre obj q)
@@ -485,13 +487,14 @@ struct
| C_int _ | C_float _ | C_pointer _ ->
let value = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
let init = Lang.freshvar ~basename:"i" (Lang.init_of_object obj) in
- [ updated_init seq loc (e_var init) ;
+ [ updated_init_atom seq loc (e_var init) ;
updated_atom seq obj loc (e_var value) ]
| C_comp _ | C_array _ ->
- havoc seq obj loc
+ havoc seq obj loc @ havoc_init seq obj loc
let assigned_range s obj l a b =
- havoc_length s obj (M.shift l obj a) (e_range a b)
+ havoc_length s obj (M.shift l obj a) (e_range a b) @
+ 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) ::
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index f9361d25ad4..2cd1ed7a5db 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -75,8 +75,10 @@ sig
val store_float : Sigma.t -> c_float -> loc -> term -> Chunk.t * term
val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
- val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val is_init_atom : Sigma.t -> loc -> term
+ 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
end
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index cf2eb752f21..56849a666de 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -50,7 +50,7 @@ let f_null = Lang.extern_f ~library ~result:t_addr "null"
let f_base_offset = Lang.extern_f ~library
~category:Qed.Logic.Injection ~result:L.Int "base_offset"
-let ty_havoc = function
+let ty_fst_arg = function
| Some l :: _ -> l
| _ -> raise Not_found
@@ -60,6 +60,12 @@ let l_havoc = Qed.Engine.{
why3 = F_call "havoc" ;
}
+let l_set_init = Qed.Engine.{
+ coq = F_call "fset_init" ;
+ altergo = F_call "set_init" ;
+ why3 = F_call "set_init" ;
+ }
+
let p_valid_rd = Lang.extern_fp ~library "valid_rd"
let p_valid_rw = Lang.extern_fp ~library "valid_rw"
let p_valid_obj = Lang.extern_fp ~library "valid_obj"
@@ -67,7 +73,9 @@ let p_invalid = Lang.extern_fp ~library "invalid"
let p_separated = Lang.extern_fp ~library "separated"
let p_included = Lang.extern_fp ~library "included"
let p_eqmem = Lang.extern_fp ~library "eqmem"
-let f_havoc = Lang.extern_f ~library ~typecheck:ty_havoc ~link:l_havoc "havoc"
+let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
+let f_set_init =
+ Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_set_init "set_init"
let p_monotonic = Lang.extern_fp ~library "monotonic_init"
let f_region = Lang.extern_f ~library ~result:L.Int "region" (* base -> region *)
let p_framed = Lang.extern_fp ~library "framed" (* m-pointer -> prop *)
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index c97d67c817f..bc7ccb47ffa 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -49,6 +49,7 @@ val f_global : lfun
val f_shift : lfun
val f_offset : lfun
val f_havoc : lfun
+val f_set_init : lfun
val f_region : lfun
val f_addr_of_int : lfun (** Physical address *)
val f_int_of_addr : lfun (** Physical address *)
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 3858f34e349..1ed00876a4d 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -814,6 +814,10 @@ struct
| _ -> error "Can not store pointer values into %a" pretty loc
let set_init_atom _ _ _ = assert false
+ let set_init _obj _loc ~length _chunk ~current =
+ let _ = length in
+ let _ = current in
+ assert false
let is_init_atom _ _ = assert false
let monotonic_init _ _ = assert false
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 31c3d5fd494..c06b32a647b 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -967,13 +967,14 @@ struct
F.e_fun f_havoc [fresh;current;loc;n]
else fresh
+ let set_init obj loc ~length _chunk ~current =
+ let n = F.e_fact (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
- let p = Lang.freshvar ~basename:"p" t_addr in
- p_forall [p]
- (p_imply (p_bool (e_get m1 (e_var p))) (p_bool (e_get m2 (e_var p))))
- (* F.p_call p_monotonic [m1; m2] *)
+ F.p_call p_monotonic [m1; m2]
let eqmem obj loc _chunk m1 m2 =
F.p_call p_eqmem [m1;m2;loc;e_int (length_of_object obj)]
@@ -992,7 +993,11 @@ struct
let store_float sigma f l v = updated sigma (m_float f) l v
let store_pointer sigma _ty l v = updated sigma M_pointer l v
- let set_init_atom sigma l v = updated sigma T_init l v
+ let set_init_atom sigma l v = (* updated sigma T_init l v *)
+ let value = Sigma.value sigma T_init in
+ let current = F.e_get value l in
+ T_init, F.e_set value l (F.e_if current e_true v)
+
let is_init_atom sigma l = F.e_get (Sigma.value sigma T_init) l
end
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index 7fe0fd7ab97..0c1a3429cd0 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -69,6 +69,11 @@ theory Memory
function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a
+ function set_init (m: map addr bool) (p:addr) (a:int) : map addr bool
+
+ predicate monotonic_init(m1 m2 : map addr bool) =
+ forall p: addr. m1[p] -> m2[p]
+
predicate valid_rw (m : map int int) (p:addr) (n:int) =
n > 0 -> ( 0 < p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
@@ -104,9 +109,6 @@ theory Memory
{ base = p.base ; offset = i } <>
{ base = q.base ; offset = j }
- predicate monotonic_init(m1 m2 : map addr bool) =
- forall p: addr. m1[p] -> m2[p]
-
(* Regions *)
function region int : int
@@ -159,7 +161,15 @@ theory Memory
forall m0 m1 : map addr 'a.
forall q p : addr.
forall a : int.
- (Map.([]) (havoc m0 m1 p a) (q)) = (if (separated q 1 p a) then (Map.([]) (m1) (q)) else (Map.([]) (m0) (q)))
+ (Map.([]) (havoc m0 m1 p a) (q)) =
+ (if (separated q 1 p a) then (Map.([]) (m1) (q)) else (Map.([]) (m0) (q)))
+
+ lemma set_init_access :
+ forall m : map addr bool.
+ forall q p : addr.
+ forall a : int.
+ (Map.([]) (set_init m p a) (q)) =
+ (if (separated q 1 p a) then (Map.([]) (m) (q)) else true)
(* Physical Address *)
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
index 91aa60d7152..3746ac027bc 100644
--- a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
@@ -19,12 +19,12 @@ void test(int* x, int (*a)[2], struct C* c){
(*a)[0] = 1 ;
//@ check qed_ok: \initialized(&(*a)[0]);
//@ check unknown: \initialized(&(*a)[1]);
- //@ check unknown: \initialized(&(*a));
+ //@ check unknown: \initialized(a);
(*a)[1] = 2 ;
//@ check qed_ok: \initialized(&(*a)[0]);
//@ check qed_ok: \initialized(&(*a)[1]);
- //@ check qed_ok: \initialized(&a);
+ //@ check provable: \initialized(a);
c->x = 1 ;
//@ check qed_ok: \initialized(&c->x);
@@ -39,7 +39,7 @@ void test(int* x, int (*a)[2], struct C* c){
//@ check unknown: \initialized(c);
c->s.y = 1 ;
- //@ check qed_ok: \initialized(&c->s);
+ //@ check provable: \initialized(&c->s);
//@ check unknown: \initialized(c);
c->a[0] = c->a[1] = c->a[2] = c->a[3] = c->a[4] = c->a[5] = c->a[6] = c->a[7] = c->a[8] = 1;
@@ -47,5 +47,5 @@ void test(int* x, int (*a)[2], struct C* c){
//@ check unknown: \initialized(c);
c->a[9] = 1 ;
- //@ check qed_ok: \initialized(c);
+ //@ check provable: \initialized(c);
}
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 03af99beb44..2bfc809d161 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
@@ -14,27 +14,25 @@ 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).
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall a_4 : addr. ((m[a_4]=true) -> (a_2[a_4]=true)).
+ Have: monotonic_init(m, a_2).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
- (a_2[shift_sint32(a, i_3)]=true)))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(a, i_2)]=true)))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: forall a_4 : addr. ((a_2[a_4]=true) -> (a_3[a_4]=true)).
+ Have: monotonic_init(a_2, a_3).
(* 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_3[shift_sint32(a, i)]=true).
+Prove: IsInit_S1_S(s, a_3).
------------------------------------------------------------
@@ -59,33 +57,30 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 118):
-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_1, m, shift_sint32(a_1, 0), 10).
-Let a_3 = havoc(Init_undef_0, m, s, 11).
+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).
Assume {
Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall a_4 : addr. ((m[a_4]=true) -> (a_2[a_4]=true)).
+ Have: monotonic_init(m, a_1).
(* 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)))).
+ (a_1[shift_sint32(a, i_2)]=true)))).
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: forall a_4 : addr. ((a_2[a_4]=true) -> (a_3[a_4]=true)).
+ Have: monotonic_init(a_1, a_2).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10).
(* Else *)
Have: 10 <= i_1.
}
-Prove: (Init_undef_0[a]=true) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- (a_3[shift_sint32(a_1, i_2)]=true)))).
+Prove: IsInit_S1_S(s, a_2).
------------------------------------------------------------
@@ -112,7 +107,7 @@ Assume {
(* Goal *)
When: !invalid(Malloc_0, shift_sint32(a, i), 1).
(* Loop assigns ... *)
- Have: forall a_2 : addr. ((m[a_2]=true) -> (a_1[a_2]=true)).
+ Have: monotonic_init(m, a_1).
(* Invariant *)
Have: (0 <= i_1) /\ (i_1 <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
@@ -120,8 +115,7 @@ Assume {
(* Else *)
Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: forall a_2 : addr. ((a_1[a_2]=true) ->
- (havoc(Init_undef_1, m, s, 11)[a_2]=true)).
+ Have: monotonic_init(a_1, havoc(Init_undef_1, m, s, 11)).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10).
(* Then *)
@@ -145,7 +139,7 @@ Assume {
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall a_4 : addr. ((m[a_4]=true) -> (a_3[a_4]=true)).
+ Have: monotonic_init(m, a_3).
(* Invariant *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
@@ -153,7 +147,7 @@ Assume {
(* Else *)
Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: (forall a_4 : addr. ((a_3[a_4]=true) -> (Init_0[a_4]=true))) /\
+ Have: monotonic_init(a_3, 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))) ->
@@ -165,9 +159,7 @@ Assume {
(* Else *)
Have: 10 <= i_1.
}
-Prove: (Init_0[a]=true) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
- (Init_0[shift_sint32(a_1, i_2)]=true)))).
+Prove: IsInit_S1_S(s, Init_0).
------------------------------------------------------------
@@ -192,7 +184,7 @@ Assume {
((i_4 = 0) \/ (i_4 = 2) \/ (i_4 = 4)) /\
((i = 0) \/ (i = 2) \/ (i = 4)).
(* Loop assigns ... *)
- Have: forall a_4 : addr. ((m[a_4]=true) -> (a_3[a_4]=true)).
+ Have: monotonic_init(m, a_3).
(* Invariant *)
Have: (0 <= i_2) /\ (i_2 <= 10) /\
(forall i_5 : Z. ((0 <= i_5) -> ((i_5 < i_2) ->
@@ -200,7 +192,7 @@ Assume {
(* Else *)
Have: 10 <= i_2.
(* Loop assigns 'CHECK' *)
- Have: (forall a_4 : addr. ((a_3[a_4]=true) -> (Init_1[a_4]=true))) /\
+ Have: monotonic_init(a_3, Init_1) /\
(forall a_4 : addr.
((forall i_5 : Z. (((i_5 = 0) \/ (i_5 = 2) \/ (i_5 = 4)) ->
(shift_sint32(a_1, i_5) != a_4))) ->
@@ -243,27 +235,25 @@ 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 <- i].
+Let a_3 = a_2[a <- true].
Assume {
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall a_4 : addr. ((m[a_4]=true) -> (a_2[a_4]=true)).
+ Have: monotonic_init(m, a_2).
(* Invariant *)
- 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)))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(a_1, i_2)]=true)))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: forall a_4 : addr. ((a_2[a_4]=true) -> (a_3[a_4]=true)).
+ Have: monotonic_init(a_2, a_3).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (i=true) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (a_3[shift_sint32(a_1, i_3)]=true)))).
+Prove: IsInit_S1_S(s, a_3).
------------------------------------------------------------
@@ -285,27 +275,26 @@ Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memtyped.i, line 84)
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_2 = a_1[shift_sint32(a, 4) <- i].
+Let a_2 = shift_sint32(a, 4).
+Let a_3 = a_1[a_2 <- i | Init_undef_0[a_2]].
Assume {
- Have: 0 <= i_1.
- Have: i_1 <= 9.
- Type: is_sint32(i_2) /\ is_sint32(i_3).
+ Type: is_sint32(i_1) /\ is_sint32(i_2).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall a_3 : addr. ((m[a_3]=true) -> (a_1[a_3]=true)).
+ Have: monotonic_init(m, a_1).
(* Invariant *)
- Have: (0 <= i_2) /\ (i_2 <= 10) /\
- (forall i_4 : Z. ((0 <= i_4) -> ((i_4 < i_2) ->
- (a_1[shift_sint32(a, i_4)]=true)))).
+ Have: (0 <= i_1) /\ (i_1 <= 10) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
+ (a_1[shift_sint32(a, i_3)]=true)))).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
(* Loop assigns 'CHECK' *)
- Have: forall a_3 : addr. ((a_1[a_3]=true) -> (a_2[a_3]=true)).
+ Have: monotonic_init(a_1, a_3).
(* Else *)
- Have: 10 <= i_3.
+ Have: 10 <= i_2.
}
-Prove: (a_2[shift_sint32(a, i_1)]=true).
+Prove: IsInit_S1_S(s, a_3).
------------------------------------------------------------
@@ -338,7 +327,7 @@ Assume {
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns 'CHECK' *)
- Have: forall a_2 : addr. ((m[a_2]=true) -> (a_1[a_2]=true)).
+ Have: monotonic_init(m, a_1).
(* Invariant 'CHECK' *)
Have: (0 <= i) /\ (i <= 10) /\
(forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
@@ -362,21 +351,19 @@ 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).
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1).
+ Type: is_sint32(i).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns 'CHECK' *)
- Have: forall a_2 : addr. ((m[a_2]=true) -> (a_1[a_2]=true)).
+ Have: monotonic_init(m, a_1).
(* Invariant 'CHECK' *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i_1) ->
- (a_1[shift_sint32(a, i_2)]=true)))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (a_1[shift_sint32(a, i_1)]=true)))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
}
-Prove: (a_1[shift_sint32(a, i)]=true).
+Prove: IsInit_S1_S(s, a_1).
------------------------------------------------------------
@@ -406,25 +393,23 @@ 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, a_1, shift_sint32(a, 1), 4).
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Heap *)
Type: region(s.base) <= 0.
(* Loop assigns ... *)
- Have: forall a_3 : addr. ((m[a_3]=true) -> (a_1[a_3]=true)).
+ Have: monotonic_init(m, a_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) ->
- (a_1[shift_sint32(a, i_3)]=true)))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_1[shift_sint32(a, i_2)]=true)))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: forall a_3 : addr. ((a_1[a_3]=true) -> (a_2[a_3]=true)).
+ Have: monotonic_init(a_1, a_2).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (a_2[shift_sint32(a, i)]=true).
+Prove: IsInit_S1_S(s, a_2).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
index a68ba3f09fd..4413fb51643 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
@@ -14,24 +14,14 @@ Prove: (Init_0[x]=true).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 13):
-Assume {
- (* Heap *)
- Type: region(a.base) <= 0.
- (* Goal *)
- When: (0 <= i) /\ (i <= 1).
-}
-Prove: (Init_0[shift_sint32(a, i)]=true).
+Assume { (* Heap *) Type: region(a.base) <= 0. }
+Prove: IsInitArray1_int(a, 2, Init_0).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 14):
-Let a = shiftfield_F2_C_s(c).
Assume { (* Heap *) Type: region(c.base) <= 0. }
-Prove: (Init_0[shiftfield_F2_C_x(c)]=true) /\
- (Init_0[shiftfield_F1_S_x(a)]=true) /\
- (Init_0[shiftfield_F1_S_y(a)]=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) ->
- (Init_0[shift_sint32(shiftfield_F2_C_a(c), i)]=true)))).
+Prove: IsInit_S2_C(c, Init_0).
------------------------------------------------------------
@@ -52,13 +42,8 @@ Prove: (Init_0[x <- true][shift_sint32(a, 1)]=true).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 22):
-Assume {
- (* Heap *)
- Type: (region(a.base) <= 0) /\ (region(x.base) <= 0).
- (* Goal *)
- When: (0 <= i) /\ (i <= 1).
-}
-Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, i)]=true).
+Assume { (* Heap *) Type: (region(a.base) <= 0) /\ (region(x.base) <= 0). }
+Prove: IsInitArray1_int(a, 2, Init_0[x <- true][shift_sint32(a, 0) <- true]).
------------------------------------------------------------
@@ -72,8 +57,11 @@ Prove: true.
------------------------------------------------------------
-Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 27):
-Prove: true.
+Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 27):
+Assume { (* Heap *) Type: (region(a.base) <= 0) /\ (region(x.base) <= 0). }
+Prove: IsInitArray1_int(a, 2,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true]).
------------------------------------------------------------
@@ -83,15 +71,14 @@ Prove: true.
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 31):
-Let m = Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true].
-Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: (m[shiftfield_F1_S_x(a_1)]=true) /\ (m[shiftfield_F1_S_y(a_1)]=true).
+Prove: IsInit_S1_S(shiftfield_F2_C_s(c),
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true]).
------------------------------------------------------------
@@ -100,28 +87,22 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
- (* Goal *)
- When: (0 <= i) /\ (i <= 9).
}
-Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true]
- [shift_sint32(shiftfield_F2_C_a(c), i)]=true).
+Prove: IsInitArray1_int(shiftfield_F2_C_a(c), 10,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true]).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 33):
-Let m = Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true].
-Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: (m[shiftfield_F1_S_x(a_1)]=true) /\
- (m[shiftfield_F1_S_y(a_1)]=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) ->
- (m[shiftfield_F2_C_x(c) <- true][shift_sint32(shiftfield_F2_C_a(c), i)]=true)))).
+Prove: IsInit_S2_C(c,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true]).
------------------------------------------------------------
@@ -142,50 +123,57 @@ Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 38):
+Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F1_S_y(shiftfield_F2_C_s(c))]=true).
+Prove: IsInit_S1_S(a_1,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+ <- true]).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 39):
-Let m = Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true].
-Let a_1 = shiftfield_F2_C_s(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: (m[shiftfield_F1_S_y(a_1)]=true) /\
- (forall i : Z. ((0 <= i) -> ((i <= 9) ->
- (m[shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1) <- true]
- [shift_sint32(shiftfield_F2_C_a(c), i)]=true)))).
+Prove: IsInit_S2_C(c,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true]
+ [shiftfield_F1_S_x(shiftfield_F2_C_s(c)) <- true]).
------------------------------------------------------------
-Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 42):
-Prove: true.
+Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 42):
+Let a_1 = shiftfield_F2_C_s(c).
+Assume {
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+ (region(x.base) <= 0).
+}
+Prove: IsInit_S1_S(a_1,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+ <- true][shiftfield_F1_S_y(a_1) <- true]).
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 43):
Let a_1 = shiftfield_F2_C_s(c).
Assume {
- Have: 0 <= i.
- Have: i <= 9.
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
- <- true][shiftfield_F1_S_y(a_1) <- true]
- [shift_sint32(shiftfield_F2_C_a(c), i)]=true).
+Prove: IsInit_S2_C(c,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+ <- true][shiftfield_F1_S_y(a_1) <- true]).
------------------------------------------------------------
@@ -211,17 +199,41 @@ Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
------------------------------------------------------------
Goal Check 'unknown' (file tests/wp_acsl/initialized_memtyped.i, line 47):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = shiftfield_F2_C_a(c).
Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
(region(x.base) <= 0).
}
-Prove: (Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
- <- true][shift_sint32(shiftfield_F2_C_a(c), 9)]=true).
+Prove: IsInit_S2_C(c,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+ <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
+ <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
+ <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
+ <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
+ <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
+ <- true]).
------------------------------------------------------------
-Goal Check 'qed_ok' (file tests/wp_acsl/initialized_memtyped.i, line 50):
-Prove: true.
+Goal Check 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 50):
+Let a_1 = shiftfield_F2_C_s(c).
+Let a_2 = shiftfield_F2_C_a(c).
+Assume {
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(c.base) <= 0) /\
+ (region(x.base) <= 0).
+}
+Prove: IsInit_S2_C(c,
+ Init_0[x <- true][shift_sint32(a, 0) <- true][shift_sint32(a, 1)
+ <- true][shiftfield_F2_C_x(c) <- true][shiftfield_F1_S_x(a_1)
+ <- true][shiftfield_F1_S_y(a_1) <- true][shift_sint32(a_2, 8)
+ <- true][shift_sint32(a_2, 7) <- true][shift_sint32(a_2, 6)
+ <- true][shift_sint32(a_2, 5) <- true][shift_sint32(a_2, 4)
+ <- true][shift_sint32(a_2, 3) <- true][shift_sint32(a_2, 2)
+ <- true][shift_sint32(a_2, 1) <- true][shift_sint32(a_2, 0)
+ <- true][shift_sint32(a_2, 9) <- true]).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
index f0add8dd99f..1ca929dd05a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.res.oracle
@@ -13,24 +13,24 @@
[wp] [Alt-Ergo] Goal typed_test_check_unknown_5 : Unsuccess
[wp] [Qed] Goal typed_test_check_qed_ok_3 : Valid
[wp] [Qed] Goal typed_test_check_qed_ok_4 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_provable : Valid
[wp] [Qed] Goal typed_test_check_qed_ok_5 : Valid
-[wp] [Qed] Goal typed_test_check_qed_ok_6 : Valid
[wp] [Alt-Ergo] Goal typed_test_check_unknown_6 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_7 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_8 : Unsuccess
-[wp] [Qed] Goal typed_test_check_qed_ok_7 : Valid
+[wp] [Qed] Goal typed_test_check_qed_ok_6 : Valid
[wp] [Alt-Ergo] Goal typed_test_check_unknown_9 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_10 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_11 : Unsuccess
-[wp] [Qed] Goal typed_test_check_qed_ok_8 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_provable_2 : Valid
[wp] [Alt-Ergo] Goal typed_test_check_unknown_12 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_test_check_provable : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_provable_3 : Valid
[wp] [Alt-Ergo] Goal typed_test_check_unknown_13 : Unsuccess
-[wp] [Qed] Goal typed_test_check_qed_ok_9 : Valid
+[wp] [Alt-Ergo] Goal typed_test_check_provable_4 : Valid
[wp] Proved goals: 10 / 23
- Qed: 9
- Alt-Ergo: 1 (unsuccess: 13)
+ Qed: 6
+ Alt-Ergo: 4 (unsuccess: 13)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- test 9 1 23 43.5%
+ test 6 4 23 43.5%
------------------------------------------------------------
--
GitLab