From e59915796c299da219c4cc265cec4a7ca65b89e2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 29 Apr 2020 15:21:58 +0200
Subject: [PATCH] [wp] Improves MemVar assigned + fixes range on comp
---
src/plugins/wp/MemVar.ml | 59 +++++-----
.../assigned_initialized_memvar.res.oracle | 101 +++++++++++-------
.../assigned_initialized_memtyped.res.oracle | 1 -
.../0bca5f490c163f9a2d1bc5be85a938cb.json | 2 +-
.../0ea068d1821f3b958beb619aabd2bf71.json | 2 -
.../26f2bec626edf9f3b21ce506a0dbc878.json | 2 -
.../2ff76ae8947b7c9d0efda0d01090aeec.json | 2 +
.../32c205ac1281122e19bed393f47b07af.json | 2 +
.../47fdc2d6da39295871208bb185768ba9.json | 2 -
.../5829cd050c6e5edf4241b52cfb347dbc.json | 2 -
.../7790b93ea943473c622f27192935dc0e.json | 2 +
.../81f6bbec14f78ded8be06b4d83acbdca.json | 2 -
.../9fc719583241f8c265dc2b57924b4e5c.json | 2 +
.../ad4c4ee63d285e19bebf51be10f2d5da.json | 2 +-
.../c17ff689fb984c1d15fced512cddb9f0.json | 2 -
... => ed2046f443d594d7a695098d6732bd53.json} | 0
.../f65786f87e448872f8395e84331fc2fa.json | 2 +
.../f6db810f4dc379e72d7a04df0c9b64f5.json | 2 +-
.../f84e2f80d92f69c9bae45d521a10486b.json | 2 +
.../fbb170335579f1933320c49f3fd8f1ca.json | 2 -
.../fe9862be590507dedbd24e64a535ac03.json | 2 +
.../assigned_initialized_memvar.res.oracle | 1 -
.../initialized_memtyped.res.oracle | 1 -
.../initialized_memvar.res.oracle | 1 -
24 files changed, 116 insertions(+), 82 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/5829cd050c6e5edf4241b52cfb347dbc.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json
rename src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/{532fc8247c18cc12fc05c6dca37a85df.json => ed2046f443d594d7a695098d6732bd53.json} (100%)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json
delete mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 18b4f8959f7..c80e3d856df 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1046,12 +1046,13 @@ struct
let sub = initialized_loc sigma obj x ofs in
Lang.F.p_forall [v] (p_imply hyp sub)
| C_comp _ ->
- let leaf = match Extlib.last ofs with
- | Field f -> Ctypes.object_of f.ftype
- | Shift(obj, _) -> obj
+ let hd = match ofs with
+ | Field f :: _ -> Ctypes.object_of f.ftype
+ | Shift(obj, _) :: _ -> obj
+ | [] -> assert false
in
- begin match leaf with
- | C_array _ -> initialized_range sigma leaf x ofs low up
+ begin match hd with
+ | C_array _ -> initialized_range sigma hd x ofs low up
| _ -> raise ShiftMismatch
end
| _ ->
@@ -1192,6 +1193,7 @@ struct
(* -------------------------------------------------------------------------- *)
let rec assigned_path
+ kind
(hs : pred list) (* collector of properties *)
(xs : var list) (* variable quantifying the assigned location *)
(ys : var list) (* variable quantifying others locations *)
@@ -1203,14 +1205,14 @@ struct
(*TODO: optimized version for terminal [Field _] and [Index _] *)
| Field f :: ofs ->
- let cf = Cfield (f, KValue) in
+ let cf = Cfield (f, kind) in
let af = e_getfield a cf in
let bf = e_getfield b cf in
- let hs = assigned_path hs xs ys af bf ofs in
+ let hs = assigned_path kind hs xs ys af bf ofs in
List.fold_left
(fun hs g ->
if Fieldinfo.equal f g then hs else
- let cg = Cfield (g, KValue) in
+ let cg = Cfield (g, kind) in
let ag = e_getfield a cg in
let bg = e_getfield b cg in
let eqg = p_forall ys (p_equal ag bg) in
@@ -1225,7 +1227,7 @@ struct
if List.exists (fun x -> F.occurs x e) xs then
(* index [e] is covered by [xs]:
must explore deeper the remaining path. *)
- assigned_path hs xs (y::ys) ak bk ofs
+ assigned_path kind hs xs (y::ys) ak bk ofs
else
(* index [e] is not covered by [xs]:
any index different from e is disjoint.
@@ -1234,7 +1236,7 @@ struct
let be = e_get b e in
let ek = p_neq e k in
let eqk = p_forall (y::ys) (p_imply ek (p_equal ak bk)) in
- assigned_path (eqk :: hs) xs ys ae be ofs
+ assigned_path kind (eqk :: hs) xs ys ae be ofs
let assigned_genset s xs mem x ofs p =
let valid = valid_offset_path s.post Sigs.RW mem x ofs in
@@ -1243,9 +1245,24 @@ struct
let a_ofs = access a ofs in
let b_ofs = access b ofs in
let p_sloc = p_forall xs (p_hyps [valid;p_not p] (p_equal a_ofs b_ofs)) in
- let conds = assigned_path [p_sloc] xs [] a b ofs in
+ let conds = assigned_path KValue [p_sloc] xs [] a b ofs in
List.map (fun p -> Assert p) conds
+ let monotonic_initialized_genset s xs mem x ofs p =
+ if x.vformal || x.vglob 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
+ let b = get_init_term s.post x in
+ let a_ofs = access_init a ofs in
+ let b_ofs = access_init b ofs in
+ let not_p = p_forall xs (p_hyps [valid;p_not p] (p_equal a_ofs b_ofs)) in
+ let exact_p =
+ p_forall xs (p_hyps [valid; p] (p_imply (p_bool a_ofs) (p_bool b_ofs)))
+ in
+ let conds = assigned_path KInit [not_p; exact_p] xs [] a b ofs in
+ List.map (fun p -> Assert p) conds
+
(* -------------------------------------------------------------------------- *)
(* --- Assigned --- *)
(* -------------------------------------------------------------------------- *)
@@ -1263,14 +1280,14 @@ struct
| None -> unsized_array ()
| Some { arr_size } -> arr_size
in
- let low = (e_int 0) in
- let up = (e_int (size-1)) in
let v = Lang.freshvar ~basename:"i" Lang.t_int in
- let hyp = p_and (p_leq low (e_var v)) (p_leq (e_var v) up) in
let obj = Ctypes.object_of t in
let ofs = ofs @ [ Shift(obj, e_var v) ] in
- let sub = monotonic_initialized seq obj x ofs in
- Lang.F.p_forall [v] (p_imply hyp sub)
+ let low = Some (e_int 0) in
+ let up = Some (e_int (size-1)) in
+ 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 ci ->
let mk_pred f =
let obj = Ctypes.object_of f.ftype in
@@ -1331,10 +1348,7 @@ struct
let k = Lang.freshvar ~basename:"k" Qed.Logic.Int in
let p = Vset.in_range (e_var k) a b in
let ofs = ofs_shift elt (e_var k) ofs in
- let obj_x = Ctypes.object_of x.vtype in
- let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj_x)) in
- Assert(monotonic_initialized seq obj_x x []) ::
- (memvar_set_init seq x [] init) @
+ (monotonic_initialized_genset seq [k] m x ofs p) @
(assigned_genset seq [k] m x ofs p)
let assigned_descr seq obj xs l p =
@@ -1345,10 +1359,7 @@ struct
| Val((HEAP|CTXT|CARR) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sdescr(xs,mloc_of_path m x ofs,p))
| Val((CVAL|CREF) as m,x,ofs) ->
- let obj_x = Ctypes.object_of x.vtype in
- let init = e_var (Lang.freshvar ~basename:"v" (init_of_object obj_x)) in
- Assert(monotonic_initialized seq obj_x x []) ::
- (memvar_set_init seq x [] init) @
+ (monotonic_initialized_genset seq xs m x ofs p) @
(assigned_genset seq xs m x ofs p)
let assigned seq obj = function
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 71276a1d27b..ed0a5eb4569 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
@@ -83,10 +83,12 @@ Assume {
Have: 10 <= i_1.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((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))))) /\
(forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (((i_3 <= 0) \/ (5 <= i_3)) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))).
+ (((i_3 <= 0) \/ (5 <= i_3)) -> ((a[i_3]=true) <-> (v[i_3]=true)))))) /\
+ (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
+ (((i_3 <= 0) \/ (5 <= i_3)) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))) /\
+ (forall i_3 : Z. ((0 < i_3) -> ((0 <= i_3) -> ((i_3 <= 4) ->
+ ((i_3 <= 9) -> ((v[i_3]=true) -> (a[i_3]=true))))))).
(* Else *)
Have: 10 <= i_2.
}
@@ -109,10 +111,12 @@ Assume {
Have: 10 <= i_1.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) -> ((v[i_4]=true) ->
- (a[i_4]=true))))) /\
(forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
- (((i_4 <= 0) \/ (5 <= i_4)) -> ((s.F1_S_a)[i_4] = v_1[i_4]))))).
+ (((i_4 <= 0) \/ (5 <= i_4)) -> ((a[i_4]=true) <-> (v[i_4]=true)))))) /\
+ (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
+ (((i_4 <= 0) \/ (5 <= i_4)) -> ((s.F1_S_a)[i_4] = v_1[i_4]))))) /\
+ (forall i_4 : Z. ((0 < i_4) -> ((0 <= i_4) -> ((i_4 <= 4) ->
+ ((i_4 <= 9) -> ((v[i_4]=true) -> (a[i_4]=true))))))).
(* Else *)
Have: 10 <= i_2.
(* Else *)
@@ -136,10 +140,12 @@ Assume {
Have: 10 <= i_1.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) -> ((v[i_4]=true) ->
- (a[i_4]=true))))) /\
(forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
- (((i_4 <= 0) \/ (5 <= i_4)) -> ((s.F1_S_a)[i_4] = v_1[i_4]))))).
+ (((i_4 <= 0) \/ (5 <= i_4)) -> ((a[i_4]=true) <-> (v[i_4]=true)))))) /\
+ (forall i_4 : Z. ((0 <= i_4) -> ((i_4 <= 9) ->
+ (((i_4 <= 0) \/ (5 <= i_4)) -> ((s.F1_S_a)[i_4] = v_1[i_4]))))) /\
+ (forall i_4 : Z. ((0 < i_4) -> ((0 <= i_4) -> ((i_4 <= 4) ->
+ ((i_4 <= 9) -> ((v[i_4]=true) -> (a[i_4]=true))))))).
(* Else *)
Have: 10 <= i_2.
(* Else *)
@@ -176,10 +182,12 @@ Assume {
Have: 10 <= i_1.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) -> ((v_1[i_5]=true) ->
- (a[i_5]=true))))) /\
(forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
- (((i_5 <= 0) \/ (5 <= i_5)) -> ((s.F1_S_a)[i_5] = v_2[i_5]))))).
+ (((i_5 <= 0) \/ (5 <= i_5)) -> ((a[i_5]=true) <-> (v_1[i_5]=true)))))) /\
+ (forall i_5 : Z. ((0 <= i_5) -> ((i_5 <= 9) ->
+ (((i_5 <= 0) \/ (5 <= i_5)) -> ((s.F1_S_a)[i_5] = v_2[i_5]))))) /\
+ (forall i_5 : Z. ((0 < i_5) -> ((0 <= i_5) -> ((i_5 <= 4) ->
+ ((i_5 <= 9) -> ((v_1[i_5]=true) -> (a[i_5]=true))))))).
(* Else *)
Have: 10 <= i_2.
(* Else *)
@@ -212,10 +220,12 @@ Assume {
Have: 10 <= i_1.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((v_2[i_6]=true) ->
- (a[i_6]=true))))) /\
(forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
- (((i_6 <= 0) \/ (5 <= i_6)) -> ((s.F1_S_a)[i_6] = v_3[i_6]))))).
+ (((i_6 <= 0) \/ (5 <= i_6)) -> ((a[i_6]=true) <-> (v_2[i_6]=true)))))) /\
+ (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
+ (((i_6 <= 0) \/ (5 <= i_6)) -> ((s.F1_S_a)[i_6] = v_3[i_6]))))) /\
+ (forall i_6 : Z. ((0 < i_6) -> ((0 <= i_6) -> ((i_6 <= 4) ->
+ ((i_6 <= 9) -> ((v_2[i_6]=true) -> (a[i_6]=true))))))).
(* Else *)
Have: 10 <= i_2.
(* Else *)
@@ -238,6 +248,7 @@ Prove: (v[4 <- v_1][i]=true).
Goal Check (file tests/wp_acsl/assigned_initialized_memvar.i, line 54):
Let a = Init_s_0.Init_F1_S_a.
+Let m = v_2[4 <- v_3].
Let a_1 = Init_s_1.Init_F1_S_a.
Assume {
Have: 0 <= i.
@@ -253,10 +264,12 @@ Assume {
Have: 10 <= i_1.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_1.Init_F1_S_i)=true) /\
- (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) -> ((v[i_7]=true) ->
- (a_1[i_7]=true))))) /\
(forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
- (((i_7 <= 0) \/ (5 <= i_7)) -> ((s.F1_S_a)[i_7] = v_1[i_7]))))).
+ (((i_7 <= 0) \/ (5 <= i_7)) -> ((a_1[i_7]=true) <-> (v[i_7]=true)))))) /\
+ (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
+ (((i_7 <= 0) \/ (5 <= i_7)) -> ((s.F1_S_a)[i_7] = v_1[i_7]))))) /\
+ (forall i_7 : Z. ((0 < i_7) -> ((0 <= i_7) -> ((i_7 <= 4) ->
+ ((i_7 <= 9) -> ((v[i_7]=true) -> (a_1[i_7]=true))))))).
(* Else *)
Have: 10 <= i_2.
(* Else *)
@@ -274,11 +287,13 @@ Assume {
Have: 10 <= i_5.
(* Loop assigns ... *)
Have: ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) ->
- ((v_2[4 <- v_3][i_7]=true) -> (a[i_7]=true))))) /\
+ (forall i_7 : Z. ((i_7 != 0) -> ((i_7 != 2) -> ((i_7 != 4) ->
+ ((0 <= i_7) -> ((i_7 <= 9) -> ((a[i_7]=true) <-> (m[i_7]=true)))))))) /\
(forall i_7 : Z. ((i_7 != 0) -> ((i_7 != 2) -> ((i_7 != 4) ->
((0 <= i_7) -> ((i_7 <= 9) ->
- ((s_1.F1_S_a)[i_7] = v_4[4 <- v_5][i_7]))))))).
+ ((s_1.F1_S_a)[i_7] = v_4[4 <- v_5][i_7]))))))) /\
+ (forall i_7 : Z. ((0 <= i_7) -> ((i_7 <= 9) -> ((m[i_7]=true) ->
+ (((i_7 = 0) \/ (i_7 = 2) \/ (i_7 = 4)) -> (a[i_7]=true)))))).
(* Else *)
Have: 10 <= i_6.
}
@@ -287,7 +302,9 @@ Prove: (a[i]=true).
------------------------------------------------------------
Goal Check 'SMOKE' (file tests/wp_acsl/assigned_initialized_memvar.i, line 55):
-Let a = Init_s_0.Init_F1_S_a.
+Let a = Init_s_1.Init_F1_S_a.
+Let m = v_2[4 <- v_3].
+Let a_1 = Init_s_0.Init_F1_S_a.
Assume {
Type: is_sint32(i) /\ is_sint32(i_1) /\ is_sint32(i_2) /\ is_sint32(i_3) /\
is_sint32(i_4) /\ is_sint32(i_5).
@@ -300,16 +317,18 @@ Assume {
Have: 10 <= i.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((v[i_6]=true) ->
- (a[i_6]=true))))) /\
(forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
- (((i_6 <= 0) \/ (5 <= i_6)) -> ((s.F1_S_a)[i_6] = v_1[i_6]))))).
+ (((i_6 <= 0) \/ (5 <= i_6)) -> ((a_1[i_6]=true) <-> (v[i_6]=true)))))) /\
+ (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
+ (((i_6 <= 0) \/ (5 <= i_6)) -> ((s.F1_S_a)[i_6] = v_1[i_6]))))) /\
+ (forall i_6 : Z. ((0 < i_6) -> ((0 <= i_6) -> ((i_6 <= 4) ->
+ ((i_6 <= 9) -> ((v[i_6]=true) -> (a_1[i_6]=true))))))).
(* Else *)
Have: 10 <= i_1.
(* Else *)
Have: 10 <= i_2.
(* Loop assigns ... *)
- Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((a[i_6]=true) ->
+ Have: forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((a_1[i_6]=true) ->
(v_2[i_6]=true)))).
(* Invariant *)
Have: (0 <= i_3) /\ (i_3 <= 10).
@@ -321,11 +340,13 @@ Assume {
Have: 10 <= i_4.
(* Loop assigns ... *)
Have: ((Init_s_1.Init_F1_S_i)=true) /\
- (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) ->
- ((v_2[4 <- v_3][i_6]=true) -> ((Init_s_1.Init_F1_S_a)[i_6]=true))))) /\
+ (forall i_6 : Z. ((i_6 != 0) -> ((i_6 != 2) -> ((i_6 != 4) ->
+ ((0 <= i_6) -> ((i_6 <= 9) -> ((a[i_6]=true) <-> (m[i_6]=true)))))))) /\
(forall i_6 : Z. ((i_6 != 0) -> ((i_6 != 2) -> ((i_6 != 4) ->
((0 <= i_6) -> ((i_6 <= 9) ->
- ((s_1.F1_S_a)[i_6] = v_4[4 <- v_5][i_6]))))))).
+ ((s_1.F1_S_a)[i_6] = v_4[4 <- v_5][i_6]))))))) /\
+ (forall i_6 : Z. ((0 <= i_6) -> ((i_6 <= 9) -> ((m[i_6]=true) ->
+ (((i_6 = 0) \/ (i_6 = 2) \/ (i_6 = 4)) -> (a[i_6]=true)))))).
(* Else *)
Have: 10 <= i_5.
}
@@ -377,7 +398,9 @@ Prove: true.
Goal Loop assigns (file tests/wp_acsl/assigned_initialized_memvar.i, line 49) (2/5):
Effect at line 50
-Let a = Init_s_0.Init_F1_S_a.
+Let a = Init_s_1.Init_F1_S_a.
+Let m = v_2[4 <- v_3].
+Let a_1 = Init_s_0.Init_F1_S_a.
Assume {
Type: is_sint32(i_2) /\ is_sint32(i_3) /\ is_sint32(i_4) /\
is_sint32(i_5) /\ is_sint32(i_6) /\ is_sint32(i_7).
@@ -393,16 +416,18 @@ Assume {
Have: 10 <= i_2.
(* Loop assigns ... *)
Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((v[i_9]=true) ->
- (a[i_9]=true))))) /\
(forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) ->
- (((i_9 <= 0) \/ (5 <= i_9)) -> ((s.F1_S_a)[i_9] = v_1[i_9]))))).
+ (((i_9 <= 0) \/ (5 <= i_9)) -> ((a_1[i_9]=true) <-> (v[i_9]=true)))))) /\
+ (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) ->
+ (((i_9 <= 0) \/ (5 <= i_9)) -> ((s.F1_S_a)[i_9] = v_1[i_9]))))) /\
+ (forall i_9 : Z. ((0 < i_9) -> ((0 <= i_9) -> ((i_9 <= 4) ->
+ ((i_9 <= 9) -> ((v[i_9]=true) -> (a_1[i_9]=true))))))).
(* Else *)
Have: 10 <= i_3.
(* Else *)
Have: 10 <= i_4.
(* Loop assigns ... *)
- Have: forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((a[i_9]=true) ->
+ Have: forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((a_1[i_9]=true) ->
(v_2[i_9]=true)))).
(* Invariant *)
Have: (0 <= i_5) /\ (i_5 <= 10).
@@ -414,11 +439,13 @@ Assume {
Have: 10 <= i_6.
(* Loop assigns ... *)
Have: ((Init_s_1.Init_F1_S_i)=true) /\
- (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) ->
- ((v_2[4 <- v_3][i_9]=true) -> ((Init_s_1.Init_F1_S_a)[i_9]=true))))) /\
+ (forall i_9 : Z. ((i_9 != 0) -> ((i_9 != 2) -> ((i_9 != 4) ->
+ ((0 <= i_9) -> ((i_9 <= 9) -> ((a[i_9]=true) <-> (m[i_9]=true)))))))) /\
(forall i_9 : Z. ((i_9 != 0) -> ((i_9 != 2) -> ((i_9 != 4) ->
((0 <= i_9) -> ((i_9 <= 9) ->
- ((s_1.F1_S_a)[i_9] = v_4[4 <- v_5][i_9]))))))).
+ ((s_1.F1_S_a)[i_9] = v_4[4 <- v_5][i_9]))))))) /\
+ (forall i_9 : Z. ((0 <= i_9) -> ((i_9 <= 9) -> ((m[i_9]=true) ->
+ (((i_9 = 0) \/ (i_9 = 2) \/ (i_9 = 4)) -> (a[i_9]=true)))))).
(* Then *)
Have: i_7 <= 9.
}
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 8d8c5b5b37c..290341bb670 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
@@ -4,7 +4,6 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 32 goals scheduled
-[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memtyped.0.session'
[wp] [Alt-Ergo] Goal typed_main_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_main_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_main_loop_invariant_2_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
index 81296a4df59..ea3a6ca498d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0bca5f490c163f9a2d1bc5be85a938cb.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0044,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0065,
"steps": 13 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json
deleted file mode 100644
index 27cea6ffc6d..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/0ea068d1821f3b958beb619aabd2bf71.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0051,
- "steps": 47 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json
deleted file mode 100644
index 6d1863edc63..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/26f2bec626edf9f3b21ce506a0dbc878.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0074,
- "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json
new file mode 100644
index 00000000000..5b4e2cd3379
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/2ff76ae8947b7c9d0efda0d01090aeec.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0107,
+ "steps": 27 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json
new file mode 100644
index 00000000000..d542926cdcc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/32c205ac1281122e19bed393f47b07af.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.008,
+ "steps": 29 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json
deleted file mode 100644
index 119359e0f31..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/47fdc2d6da39295871208bb185768ba9.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0023,
- "steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/5829cd050c6e5edf4241b52cfb347dbc.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/5829cd050c6e5edf4241b52cfb347dbc.json
deleted file mode 100644
index bab04bc361e..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/5829cd050c6e5edf4241b52cfb347dbc.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0094,
- "steps": 39 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json
new file mode 100644
index 00000000000..91964651c8d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/7790b93ea943473c622f27192935dc0e.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0227,
+ "steps": 94 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json
deleted file mode 100644
index 53ba6839db5..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/81f6bbec14f78ded8be06b4d83acbdca.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0057,
- "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json
new file mode 100644
index 00000000000..a445667f615
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/9fc719583241f8c265dc2b57924b4e5c.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0091,
+ "steps": 42 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json
index 81d5e9d2f02..c5053a8333f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ad4c4ee63d285e19bebf51be10f2d5da.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0066,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0072,
"steps": 18 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json
deleted file mode 100644
index 0e6c81c0a50..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/c17ff689fb984c1d15fced512cddb9f0.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0082,
- "steps": 25 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/532fc8247c18cc12fc05c6dca37a85df.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ed2046f443d594d7a695098d6732bd53.json
similarity index 100%
rename from src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/532fc8247c18cc12fc05c6dca37a85df.json
rename to src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/ed2046f443d594d7a695098d6732bd53.json
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json
new file mode 100644
index 00000000000..94e34ea6e49
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f65786f87e448872f8395e84331fc2fa.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0077,
+ "steps": 33 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json
index 4f004cd73a5..0f8cdb45879 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f6db810f4dc379e72d7a04df0c9b64f5.json
@@ -1,2 +1,2 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0048,
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0046,
"steps": 11 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json
new file mode 100644
index 00000000000..152e6b163fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/f84e2f80d92f69c9bae45d521a10486b.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0018,
+ "steps": 21 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json
deleted file mode 100644
index 9059ef12849..00000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fbb170335579f1933320c49f3fd8f1ca.json
+++ /dev/null
@@ -1,2 +0,0 @@
-{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0081,
- "steps": 20 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json
new file mode 100644
index 00000000000..c4f419fb791
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session/cache/fe9862be590507dedbd24e64a535ac03.json
@@ -0,0 +1,2 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0087,
+ "steps": 39 }
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 1e4969d23d8..5184840f613 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
@@ -4,7 +4,6 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 25 goals scheduled
-[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigned_initialized_memvar.0.session'
[wp] [Alt-Ergo] Goal typed_main_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_main_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_main_loop_invariant_2_preserved : Valid
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 003c83000b9..b27ea93eec7 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
@@ -4,7 +4,6 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
-[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memtyped.0.session'
[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
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 1f5d08de549..ea40fb15e88 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
@@ -7,7 +7,6 @@
[wp] [Qed] Goal typed_globals_check_qed_ok : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_2 : Valid
[wp] [Qed] Goal typed_globals_check_qed_ok_3 : Valid
-[wp] Warning: creating session directory `/home/allanb/Documents/Frama-C/branches/feature/blanchard/wp/initialized/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_memvar.0.session'
[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko : Unsuccess
[wp] [Qed] Goal typed_globals_check_qed_ok_4 : Valid
[wp] [Alt-Ergo] Goal typed_globals_check_qed_ko_2 : Unsuccess
--
GitLab