diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 2776f437fd700dead55fdce850beec4d888f95fb..e373bd541e29e52019abce940537424ab03ff533 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -205,6 +205,7 @@ struct
alloc = ALLOC.create () ;
mem = M.Sigma.create () ;
}
+
let copy s = {
vars = SIGMA.copy s.vars ;
init = INIT.copy s.init ;
@@ -1293,6 +1294,7 @@ struct
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
@@ -1307,6 +1309,7 @@ struct
in
let conds = assigned_path KInit [not_p; exact_p] xs [] a b ofs in
List.map (fun p -> Assert p) conds
+ *)
(* -------------------------------------------------------------------------- *)
(* --- Assigned --- *)
@@ -1401,7 +1404,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
- (monotonic_initialized_genset seq [k] m x ofs p) @
+ (* (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 =
@@ -1412,7 +1415,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) ->
- (monotonic_initialized_genset seq xs m x ofs p) @
+ (* (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 a4e3a95a8411e0fad2073413b324aa2485515e56..a095737754b14ad8f09099416bd8bcf7bf91aa96 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
@@ -71,29 +71,24 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 105):
-Let a = Init_s_0.Init_F1_S_a.
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
- ((0 <= i_3) -> ((i_3 <= 9) -> ((a[i_3]=true) <-> (v[i_3]=true)))))))) /\
- (forall i_3 : Z. ((i_3 != 0) -> ((i_3 != 2) -> ((i_3 != 4) ->
- ((0 <= i_3) -> ((i_3 <= 9) -> ((s.F1_S_a)[i_3] = v_1[i_3]))))))) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) -> ((v[i_3]=true) ->
- (((i_3 = 0) \/ (i_3 = 2) \/ (i_3 = 4)) -> (a[i_3]=true)))))).
+ Have: ((s.F1_S_i) = 0) /\
+ (forall i_2 : Z. ((i_2 != 0) -> ((i_2 != 2) -> ((i_2 != 4) ->
+ ((0 <= i_2) -> ((i_2 <= 9) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))))).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
@@ -255,29 +250,24 @@ Prove: true.
------------------------------------------------------------
Goal Check 'CHECK' (file tests/wp_acsl/assigned_initialized_memvar.i, line 38):
-Let a = Init_s_0.Init_F1_S_a.
Assume {
- Have: 0 <= i.
- Have: i <= 9.
- Type: is_sint32(i_1) /\ is_sint32(i_2).
+ Type: is_sint32(i) /\ is_sint32(i_1).
(* Invariant *)
- Have: (0 <= i_1) /\ (i_1 <= 10) /\
- (((0 < i_1) ->
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 < i_1) -> (v[i_3]=true)))))).
+ Have: (0 <= i) /\ (i <= 10) /\
+ (((0 < i) ->
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) -> (v[i_2]=true)))))).
(* Else *)
- Have: 10 <= i_1.
+ Have: 10 <= i.
(* Loop assigns 'CHECK' *)
- Have: ((s.F1_S_i) = 0) /\ ((Init_s_0.Init_F1_S_i)=true) /\
- (forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 9) ->
- (((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))))))).
+ Have: ((s.F1_S_i) = 0) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ (((i_2 <= 0) \/ (5 <= i_2)) -> ((s.F1_S_a)[i_2] = v_1[i_2]))))).
(* Else *)
- Have: 10 <= i_2.
+ Have: 10 <= i_1.
}
-Prove: (a[i]=true).
+Prove: ((Init_s_0.Init_F1_S_i)=true) /\
+ (forall i_2 : Z. ((0 <= i_2) -> ((i_2 <= 9) ->
+ ((Init_s_0.Init_F1_S_a)[i_2]=true)))).
------------------------------------------------------------
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 bdd6cac2653343ae848ca9b820fc69dc15e8fdd7..de07c211f1cadf0a54fcd5e23b3f345692bdd7cb 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
@@ -7,7 +7,7 @@
[wp] [Qed] Goal typed_initialize_loop_invariant_CHECK_established : Valid
[wp] [Alt-Ergo] Goal typed_initialize_check_CHECK : Valid
[wp] [Qed] Goal typed_initialize_loop_assigns : Valid
-[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_range_check_CHECK : Unsuccess
[wp] [Qed] Goal typed_range_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_range_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_field_check_CHECK : Valid
@@ -17,7 +17,7 @@
[wp] [Alt-Ergo] Goal typed_index_check_CHECK : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_index_loop_assigns_part2 : Valid
-[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Valid
+[wp] [Alt-Ergo] Goal typed_descr_check_CHECK : Unsuccess
[wp] [Qed] Goal typed_descr_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_descr_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_descr_loop_assigns_part3 : Valid
@@ -25,16 +25,16 @@
[wp] [Qed] Goal typed_descr_loop_assigns_part5 : Valid
[wp] [Alt-Ergo] Goal typed_comp_check_CHECK : Valid
[wp] [Qed] Goal typed_comp_loop_assigns : Valid
-[wp] Proved goals: 22 / 22
+[wp] Proved goals: 20 / 22
Qed: 13
- Alt-Ergo: 9
+ Alt-Ergo: 7 (unsuccess: 2)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
initialize 2 2 4 100%
- range 2 1 3 100%
+ range 2 - 3 66.7%
field 1 1 2 100%
array 1 1 2 100%
index 2 1 3 100%
- descr 4 2 6 100%
+ descr 4 1 6 83.3%
comp 1 1 2 100%
------------------------------------------------------------