diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index be4aaa052a4dbdf880a9cca401901a3ec7cb8ed4..c4b348892c1c893fafd4c29e2d634e9beb436ce4 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -113,7 +113,7 @@ struct
let is_exp_range sigma l obj a b v =
let x = Lang.freshvar ~basename:"k" Logic.Int in
let k = e_var x in
- let range = [ p_leq a k ; p_lt k b ] in
+ let range = [ p_leq a k ; p_leq k b ] in
let init =
match v with
| None -> is_zero sigma obj (M.shift l obj k)
@@ -443,31 +443,35 @@ struct
~severe:false ~effect:"Skip initializer"
(fun () ->
let l = lval sigma lv in
- match init with
- | Some e ->
- let v = M.load sigma obj l in
- p_equal (val_of_exp sigma e) (cval v)
- | None -> is_zero sigma obj l
+ let value_hyp = match init with
+ | Some e ->
+ let v = M.load sigma obj l in
+ p_equal (val_of_exp sigma e) (cval v)
+ | None -> is_zero sigma obj l
+ in
+ value_hyp, (M.initialized sigma (Rloc(obj, l)))
) () in
match outcome with
- | Warning.Failed warn -> warn , F.p_true
+ | Warning.Failed warn -> warn , (F.p_true, F.p_true)
| Warning.Result(warn , hyp) -> warn , hyp
- let init_range ~sigma lv typ a b value =
+ let init_range ~sigma lv typ low up value =
let obj = Ctypes.object_of typ in
let outcome = Warning.catch
~severe:false ~effect:"Skip initializer"
(fun () ->
let l = lval sigma lv in
let e = Extlib.opt_map (exp sigma) value in
- is_exp_range sigma l obj (e_bigint a) (e_bigint b) e
+ let low = e_bigint low and up = e_bigint up in
+ (is_exp_range sigma l obj low up e),
+ (M.initialized sigma (Rrange(l, obj, Some low, Some up)))
) () in
match outcome with
- | Warning.Failed warn -> warn , F.p_true
+ | Warning.Failed warn -> warn , (F.p_true, F.p_true)
| Warning.Result(warn , hyp) -> warn , hyp
- type warned_hyp = Warning.Set.t * Lang.F.pred
+ type warned_hyp = Warning.Set.t * (Lang.F.pred * Lang.F.pred)
(* Hypothesis for initialization of one variable *)
let rec init_variable ~sigma lv init acc =
@@ -517,8 +521,7 @@ struct
| (_,None) -> acc (* nothing was delayed *)
| (il,Some (i0,_,exp)) when Integer.lt il i0 ->
(* Added pred: \forall i \in [il .. i0] ; t[i]==exp *)
- let i2 = Integer.succ i0 in
- init_range ~sigma lv ty il i2 (Some exp) :: acc
+ init_range ~sigma lv ty il i0 (Some exp) :: acc
| (_il,Some (_i0,off,exp)) ->
(* case [_il=_i0], so uses [off] corresponding to [_i0]
Added pred: t[i]==exp*)
@@ -531,7 +534,7 @@ struct
if Integer.ge i0 i1 then (* no hole *) acc
else (* defaults values
Added pred: \forall i \in [i0 .. i1[ ; t[i]==default *)
- init_range ~sigma lv ty i0 i1 None :: acc
+ init_range ~sigma lv ty i0 (Integer.pred i1) None :: acc
in
let acc, delayed =
List.fold_left
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 102135a390c059ec2ecddaa30e0e355e555ff18d..4bd0f123fe21fb704e8ea1f653a52364e0c23e41 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1085,11 +1085,11 @@ struct
| Ref _ -> p_true
| Loc l -> M.initialized sigma.mem (Rloc(obj,l))
| Val(m,x,p) ->
- if (x.vformal || x.vglob) then
+ if is_heap_allocated m then
+ M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
+ else if (x.vformal || x.vglob) then
try valid_offset RW (vobject m x) p
with ShiftMismatch -> shift_mismatch l
- else if is_heap_allocated m then
- M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
else
initialized_loc sigma obj x p
end
@@ -1099,17 +1099,26 @@ struct
| Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
| Val(m,x,p) ->
try
- let in_array = valid_range RW (vobject m x) p (elt, a, b) in
- let initialized =
- if x.vformal || x.vglob 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)
- with ShiftMismatch ->
if is_heap_allocated m then
let l = mloc_of_loc l in
M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
- else shift_mismatch l
+ else
+ let rec normalize obj = function
+ | [] -> [], a, b
+ | [Shift(elt, i)] when Ctypes.equal obj elt ->
+ [], F.e_add a i, F.e_add b i
+ | f :: ofs ->
+ let l, a, b = normalize obj ofs in f :: l, a, b
+ in
+ 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
+ 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)
+ with ShiftMismatch ->
+ shift_mismatch l
end
| Rrange(l, _,a,b) ->
Warning.error
@@ -1190,7 +1199,10 @@ struct
match scope with
| Leave -> []
| Enter ->
- let xs = List.filter (fun v -> not v.vformal && not v.vglob) xs in
+ let xs = List.filter
+ (fun v -> 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
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index e5c252e0076a78c4833cb29d0d7ed58bdbd14a0b..1b594803754f617a5c0b63f94f1216275517fed2 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -587,7 +587,7 @@ sig
Express that all objects in a range of locations have a given value.
More precisely, [is_exp_range sigma loc ty a b v] express that
- value at [( ty* )loc + k] equals [v], forall [a <= k < b].
+ value at [( ty* )loc + k] equals [v], forall [a <= k <= b].
Value [v=None] stands for zero.
*)
val is_exp_range :
@@ -598,17 +598,25 @@ sig
val unchanged : M.sigma -> M.sigma -> varinfo -> pred
(** Express that a given variable has the same value in two memory states. *)
- type warned_hyp = Warning.Set.t * pred
-
- val init : sigma:M.sigma -> varinfo -> init option -> warned_hyp list
- (** Express that some variable has some initial value at the
- given memory state.
-
- Remark: [None] initializer are interpreted as zeroes. This is consistent
- with the [init option] associated with global variables in CIL,
- for which the default initializer are zeroes. There is no
- [init option] value associated with local initializers.
- *)
+ type warned_hyp = Warning.Set.t * (pred * pred)
+
+ val init :
+ sigma:M.sigma -> varinfo -> init option -> warned_hyp list
+ (** Express that some variable has some initial value at the
+ given memory state. The first predicate states the value,
+ the second, the initialization status.
+
+ Note: we DO NOT merge values and initialization status
+ hypotheses as the factorization performed by Qed can make
+ predicates too hard to simplify later.
+
+ Remark: [None] initializer are interpreted as zeroes. This is consistent
+ with the [init option] associated with global variables in CIL,
+ for which the default initializer are zeroes. This function is called
+ for global initializers and local initializers ([Cil.Local_init]).
+ It is not called for local variables without initializers as they do not
+ have a [Cil.init option].
+ *)
end
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 28aaa51e928def28bc856f4e00b73a7a3beb52c5..4272a3333deb1d013d8d4681454ad19a04edd7b2 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -416,7 +416,10 @@ struct
let here = Sigma.create () in
let next = Sigma.create () in
(*TODO: make something of warnings *)
- let hyp = Lang.F.p_all snd (C.init ~sigma:next vi (Some init)) in
+ let init = C.init ~sigma:next vi (Some init) in
+ let hyp_value = Lang.F.p_all (fun (_, h) -> fst h) init in
+ let hyp_init = Lang.F.p_all (fun (_, h) -> snd h) init in
+ let hyp = Lang.F.p_and hyp_init hyp_value in
effect (env @: Clabels.here) (Cfg.E.create {pre=here; post=next} hyp) (env @: Clabels.next)
| Skip _ | Code_annot _ -> goto (env @: Clabels.here) (env @: Clabels.next)
@@ -669,7 +672,10 @@ struct
let cfg_init = Globals.Vars.fold_in_file_order
(fun var initinfo cfg ->
if var.vstorage = Extern then cfg else
- let h = Lang.F.p_all snd (C.init ~sigma:sinit var initinfo.init) in
+ let init = C.init ~sigma:sinit var initinfo.init in
+ let hvalue = Lang.F.p_all (fun (_, h) -> fst h) init in
+ let hinit = Lang.F.p_all (fun (_, h) -> snd h) init in
+ let h = Lang.F.p_and hvalue hinit in
let h = Cfg.P.create
(Cfg.Node.Map.add ninit sinit Cfg.Node.Map.empty)
h
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index f5006fd95ba3ffa91d98ab0e8eee3dbaa053259a..dac25e8ec8d00a02707cc800cc423161833a4bbc 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -248,11 +248,6 @@ struct
path = path ;
}
- let assume_vcs ?descr ?filter ?init whs vc =
- List.fold_left
- (fun vc (warn,hyp) -> assume_vc ?descr ?filter ?init ~warn [hyp] vc)
- vc whs
-
(* -------------------------------------------------------------------------- *)
(* --- Branching --- *)
(* -------------------------------------------------------------------------- *)
@@ -906,13 +901,14 @@ struct
[C.unchanged shere sinit v]
in { wp with vcs = gmap const_vc wp.vcs })
- let init wenv var init wp = in_wenv wenv wp
+ let init wenv var opt_init wp = in_wenv wenv wp
(fun env wp ->
+ let assume = assume_vc ~descr:"Initializer" ~filter:true ~init:true in
let sigma = L.current env in
- let init_vc = assume_vcs
- ~init:true ~filter:true
- ~descr:"Initializer"
- (C.init ~sigma var init)
+ let init_vc vc =
+ List.fold_left
+ (fun vc (warn,(hv,hi)) -> assume ~warn [hi] (assume ~warn [hv] vc))
+ vc (C.init ~sigma var opt_init)
in { wp with vcs = gmap init_vc wp.vcs })
(* -------------------------------------------------------------------------- *)
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 d7c91e8c587cda072659f627edf1409be880ede6..d1946539852b596ec8eb961d2858433278d7c44e 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -352,7 +352,7 @@ new way
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
- Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
+ Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
@@ -370,7 +370,7 @@ Prove: foo_0 = 1.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
- Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
+ Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
@@ -387,7 +387,7 @@ Prove: true.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
- Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
+ Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
@@ -405,8 +405,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ 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: i_2 <= 10.
Have: i <= 10.
@@ -428,8 +428,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i = 0.
+ 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: i_1 <= 10.
Have: i_2 <= 10.
@@ -448,8 +448,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ 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: i_2 <= 10.
Have: i <= 10.
@@ -467,8 +467,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ 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: i_2 <= 10.
Have: i <= 10.
@@ -485,8 +485,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ 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).
}
Prove: i <= 10.
@@ -500,8 +500,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i_1 = 0.
+ 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: i_2 <= 10.
Have: i_3 <= 10.
@@ -520,8 +520,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
- Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
- Have: i = 0.
+ 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: i_1 <= 10.
Have: i_2 <= 10.
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_local_init.i b/src/plugins/wp/tests/wp_acsl/initialized_local_init.i
new file mode 100644
index 0000000000000000000000000000000000000000..3fe1467bc0fc358b7ca5ad95a300ae2e3d4971d3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/initialized_local_init.i
@@ -0,0 +1,19 @@
+void l_int(void){
+ int x = 1 ;
+ //@ assert SUCCS: x == 1;
+ //@ assert SUCCS: \initialized(&x);
+ //@ check FAILS: \false ;
+}
+void l_array(void){
+ int x[3] = { 0 } ;
+ //@ assert SUCCS: x[0] == x[1] == x[2] == 0 ;
+ //@ assert SUCCS: \initialized(&x);
+ //@ check FAILS: \false ;
+}
+typedef struct { int x ; char t[2] ; } S;
+void l_struct(void){
+ S s = { 0 };
+ //@ assert SUCCS: s.x == s.t[0] == s.t[1] == 0 ;
+ //@ assert SUCCS: \initialized(&s);
+ //@ check FAILS: \false ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
index b9a70c9c0fa1f8ffb2e4608de7074eac98495b30..2968325323b4f5d4dbcae428ac391914c044d9ac 100644
--- a/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
+++ b/src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
@@ -81,4 +81,10 @@ void formal(int x)
{
int * p = &x ;
//@ assert provable: \initialized(p);
-}
\ No newline at end of file
+}
+
+void ptr_on_local(void){
+ int x[3] = {0} ;
+ int *p = x ;
+ //@ assert provable: \initialized(p + (0..2));
+}
diff --git a/src/plugins/wp/tests/wp_acsl/initialized_shift_array.i b/src/plugins/wp/tests/wp_acsl/initialized_shift_array.i
new file mode 100644
index 0000000000000000000000000000000000000000..9fd5ed15b2f46b36c1baa9295f3a3cad52f4c1c8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/initialized_shift_array.i
@@ -0,0 +1,56 @@
+/*@
+ requires \initialized(buf + (0 .. count - 1));
+*/
+int test(char *buf, int count);
+
+// Success:
+
+void succ_full_first_cell(void){
+ char buf[3] = {0};
+ test(buf , 1);
+}
+void succ_full_full(void){
+ char buf[3] = {0};
+ test(&buf[0], 3);
+}
+void succ_full_from_1(void){
+ char buf[3] = {0};
+ test(buf+1 , 2);
+}
+void succ_from_1_from_1(void){
+ char buf[3];
+ buf[1] = buf[2] = 1 ;
+ test(buf+1 , 2);
+}
+void succ_full_from_2(void){
+ char buf[3] = {0};
+ test(&buf[2], 1);
+}
+
+// Failure:
+
+void fail_cell_before(void){
+ char buf[3] = {0};
+ test(buf-1 , 1);
+}
+void fail_too_long(void){
+ char buf[3] = {0};
+ test(buf , 4);
+}
+void fail_too_long_from_1(void){
+ char buf[3] = {0};
+ test(&buf[1], 3);
+}
+void fail_too_long_from_2(void){
+ char buf[3] = {0};
+ test(buf+2 , 2);
+}
+void fail_cell_after_end(void){
+ char buf[3] = {0};
+ test(buf+3 , 1);
+}
+void fail_partial_not_full(void){
+ char buf[3];
+ buf[0] = buf[1] = 0;
+ test(&buf[0], 3);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b64e2acc93c3758f0b4fd6bc7bdcec4280dd0cbe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle
@@ -0,0 +1,89 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function l_array
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 9):
+Let x_1 = x[1].
+Let x_2 = x[2].
+Assume {
+ Type: is_sint32(x_1) /\ is_sint32(x_2).
+ (* Initializer *)
+ Init: x[0] = 0.
+ (* Initializer *)
+ Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
+}
+Prove: (x_1 = 0) /\ (x_2 = 0) /\ (x_2 = x_1).
+
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 10):
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_x_0[0]=true).
+ (* Initializer *)
+ Init: x[0] = 0.
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (Init_x_0[i_1]=true))).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (x[i_1] = 0))).
+ (* Assertion 'SUCCS' *)
+ Have: (x[1] = 0) /\ (x[2] = 0).
+}
+Prove: (Init_x_0[i]=true).
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 11):
+Assume {
+ (* Initializer *)
+ Init: x[0] = 0.
+ (* Initializer *)
+ Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
+ (* Assertion 'SUCCS' *)
+ Have: (x[1] = 0) /\ (x[2] = 0).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function l_int
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 4):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 5):
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function l_struct
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 18):
+Prove: false.
+
+------------------------------------------------------------
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 106088887237948475c2ecd809f1749403db46fb..1a01091dabd2747b0fb3ad141203650bd1aa1e28 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
@@ -50,6 +50,26 @@ Goal Post-condition 'unknown' in 'glob_var':
Assume { (* Heap *) Type: (region(px_0.base) <= 0) /\ cinits(Init_0). }
Prove: (Init_0[px_0]=true).
+------------------------------------------------------------
+------------------------------------------------------------
+ Function ptr_on_local
+------------------------------------------------------------
+
+Goal Assertion 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 89):
+Let a = global(L_x_63).
+Assume {
+ (* Heap *)
+ Type: cinits(Init_0).
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_0[shift_sint32(a, 0)]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_0[shift_sint32(a, i_1)]=true))).
+}
+Prove: (Init_0[shift_sint32(a, i)]=true).
+
------------------------------------------------------------
------------------------------------------------------------
Function test
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7a9d25eed759b7fd126d959ee90cd39cb9922546
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
@@ -0,0 +1,134 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning:
+ No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function fail_cell_after_end
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_after_end' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 50)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_cell_before
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_before' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 34)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_partial_not_full
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_partial_not_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 55)
+:
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 2). }
+Prove: (([false..])[1 <- true][0 <- true][i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_too_long
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 38)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_too_long_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 42)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function fail_too_long_from_2
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_2' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 46)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_from_1_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_from_1_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 23)
+:
+Assume { (* Goal *) When: (0 < i) /\ (i <= 2). }
+Prove: (([false..])[2 <- true][1 <- true][i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_first_cell
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_first_cell' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 10)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 18)
+:
+Assume {
+ (* Goal *)
+ When: (0 < i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_buf_0[0]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_from_2
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_from_2' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 27)
+:
+Assume {
+ (* Goal *)
+ When: (2 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_buf_0[0]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[2]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function succ_full_full
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 14)
+:
+Assume {
+ (* Goal *)
+ When: (0 <= i) /\ (i <= 2).
+ (* Initializer *)
+ Init: (Init_buf_0[0]=true).
+ (* Initializer *)
+ Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+ (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[i]=true).
+
+------------------------------------------------------------
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 0a7a16a6acadb3ef41857bbbff863c300b5da1be..083f7d0ff4956ba090210e61d5f4da2817ea3822 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
@@ -251,9 +251,6 @@ Assume {
is_sint8_chunk(Mchar_0).
Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- (* Block In *)
- Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
- Init_r_0.
}
Prove: valid_rd(Malloc_0, p, 3).
@@ -273,9 +270,6 @@ Assume {
is_sint8_chunk(Mchar_0).
Type: IsS1_X(r) /\ is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
is_sint8_chunk(Mchar_0).
- (* Block In *)
- Have: ({ Init_F1_X_a = false ; Init_F1_X_b = false ; Init_F1_X_c = false }) =
- Init_r_0.
(* Assertion 'rte,mem_access' *)
Have: valid_rd(Malloc_0, p, 3).
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..86800d74f72b4a1ffb6e4354f411e1a52bbee829
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_local_init.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 9 goals scheduled
+[wp] [Qed] Goal typed_l_int_assert_SUCCS : Valid
+[wp] [Qed] Goal typed_l_int_assert_SUCCS_2 : Valid
+[wp] [Alt-Ergo] Goal typed_l_int_check_FAILS : Unsuccess
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS : Valid
+[wp] [Alt-Ergo] Goal typed_l_array_assert_SUCCS_2 : Valid
+[wp] [Alt-Ergo] Goal typed_l_array_check_FAILS : Unsuccess
+[wp] [Qed] Goal typed_l_struct_assert_SUCCS : Valid
+[wp] [Qed] Goal typed_l_struct_assert_SUCCS_2 : Valid
+[wp] [Alt-Ergo] Goal typed_l_struct_check_FAILS : Unsuccess
+[wp] Proved goals: 6 / 9
+ Qed: 4
+ Alt-Ergo: 2 (unsuccess: 3)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ l_int 2 - 3 66.7%
+ l_array - 2 3 66.7%
+ l_struct 2 - 3 66.7%
+------------------------------------------------------------
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 88684268b9cb445cdfdf9909b4e607ac18a0664f..3024322ab329f7d8824e06a8907b1fa86501f0e2 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
@@ -2,7 +2,7 @@
[kernel] Parsing tests/wp_acsl/initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 28 goals scheduled
+[wp] 29 goals scheduled
[wp] [Alt-Ergo] Goal typed_test_check_unknown : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_2 : Unsuccess
[wp] [Alt-Ergo] Goal typed_test_check_unknown_3 : Unsuccess
@@ -31,13 +31,15 @@
[wp] [Alt-Ergo] Goal typed_glob_arr_ensures_provable : Valid
[wp] [Alt-Ergo] Goal typed_glob_arr_ensures_unknown : Unsuccess
[wp] [Alt-Ergo] Goal typed_formal_assert_provable : Valid
-[wp] Proved goals: 13 / 28
+[wp] [Alt-Ergo] Goal typed_ptr_on_local_assert_provable : Valid
+[wp] Proved goals: 14 / 29
Qed: 6
- Alt-Ergo: 7 (unsuccess: 15)
+ Alt-Ergo: 8 (unsuccess: 15)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
test 6 4 23 43.5%
glob_var - 1 2 50.0%
glob_arr - 1 2 50.0%
formal - 1 1 100%
+ ptr_on_local - 1 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ca01bf0f44a9041cc0a9883e59bb919b43910f63
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
@@ -0,0 +1,35 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning:
+ No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 11 goals scheduled
+[wp] [Qed] Goal typed_succ_full_first_cell_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_full_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_from_1_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_from_1_from_1_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_from_2_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_fail_cell_before_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_from_1_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_from_2_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_cell_after_end_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_partial_not_full_call_test_requires : Unsuccess
+[wp] Proved goals: 5 / 11
+ Qed: 1
+ Alt-Ergo: 4 (unsuccess: 6)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ succ_full_first_cell 1 - 1 100%
+ succ_full_full - 1 1 100%
+ succ_full_from_1 - 1 1 100%
+ succ_from_1_from_1 - 1 1 100%
+ succ_full_from_2 - 1 1 100%
+ fail_cell_before - - 1 0.0%
+ fail_too_long - - 1 0.0%
+ fail_too_long_from_1 - - 1 0.0%
+ fail_too_long_from_2 - - 1 0.0%
+ fail_cell_after_end - - 1 0.0%
+ fail_partial_not_full - - 1 0.0%
+------------------------------------------------------------