diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 65ff69a9b88586d14ad5200049359a688a392bb6..18d0d1a9ace4418a952940ed5bfe33e1006b41b8 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -1232,13 +1232,13 @@ let is_cint_simplifier =
Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))
- method simplify_exp (e : term) = e
+ method equivalent_exp (e : term) = e
- method simplify_hyp p = self#simplify ~is_goal:false p
+ method weaker_hyp p = self#simplify ~is_goal:false p
- method simplify_goal p = self#simplify ~is_goal:true p
+ method stronger_goal p = self#simplify ~is_goal:true p
- method simplify_branch p = p
+ method equivalent_branch p = p
method infer = []
end
@@ -1292,19 +1292,19 @@ let mask_simplifier =
end
| _ -> ()) (F.e_prop p)
- method simplify_exp e =
+ method equivalent_exp e =
if Tmap.is_empty magnitude then e else
Lang.e_subst (rewrite magnitude) e
- method simplify_hyp p =
+ method weaker_hyp p =
if Tmap.is_empty magnitude then p else
Lang.p_subst (rewrite magnitude) p
- method simplify_branch p =
+ method equivalent_branch p =
if Tmap.is_empty magnitude then p else
Lang.p_subst (rewrite magnitude) p
- method simplify_goal p =
+ method stronger_goal p =
if Tmap.is_empty magnitude then p else
Lang.p_subst (rewrite magnitude) p
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index fcf91379566be92395bd50fd1d57442c5f623cc3..a8bc20956ca3a1d9699280836c97f0cbe9672085 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -880,35 +880,59 @@ and letify_case sigma ~target ~export seq =
(* --- External Simplifier --- *)
(* -------------------------------------------------------------------------- *)
-let simplify_exp solvers e =
- List.fold_left (fun e s -> s#simplify_exp e) e solvers
-let simplify_goal solvers p =
- List.fold_left (fun p s -> s#simplify_goal p) p solvers
-let simplify_hyp solvers p =
- List.fold_left (fun p s -> s#simplify_hyp p) p solvers
-let simplify_branch solvers p =
- List.fold_left (fun p s -> s#simplify_branch p) p solvers
+let equivalent_exp solvers e =
+ List.fold_left (fun e s -> s#equivalent_exp e) e solvers
+let stronger_goal solvers p =
+ List.fold_left (fun p s -> s#stronger_goal p) p solvers
+let weaker_hyp solvers p =
+ List.fold_left (fun p s -> s#weaker_hyp p) p solvers
+let equivalent_branch solvers p =
+ List.fold_left (fun p s -> s#equivalent_branch p) p solvers
+
+let apply_goal solvers p =
+ let stronger_and_then_assume p =
+ let p' = stronger_goal solvers p in
+ List.iter (fun s -> s#assume (p_not p')) solvers;
+ p'
+ in
+ match F.p_expr p with
+ | Or ps ->
+ let unmodified,qs = List.fold_left (fun (unmodified,qs) p ->
+ let p' = stronger_and_then_assume p in
+ (unmodified && (Lang.F.eqp p p')), (p'::qs))
+ (true,[]) ps
+ in if unmodified then p else p_disj qs
+ | _ -> stronger_and_then_assume p
let apply_hyp modified solvers h =
- let simple p =
- let p' = simplify_hyp solvers p in
+ let weaken_and_then_assume p =
+ let p' = weaker_hyp solvers p in
if not (Lang.F.eqp p p') then modified := true;
List.iter (fun s -> s#assume p') solvers; p'
in
+ let weaken p = match F.p_expr p with
+ | And ps ->
+ let unmodified,qs = List.fold_left (fun (unmodified,qs) p ->
+ let p' = weaken_and_then_assume p in
+ (unmodified && (Lang.F.eqp p p')), (p'::qs))
+ (true,[]) ps
+ in if unmodified then p else p_conj qs
+ | _ -> weaken_and_then_assume p
+ in
match h.condition with
- | State s -> update_cond h (State (Mstate.apply (simplify_exp solvers) s))
- | Init p -> update_cond h (Init (simple p))
- | Type p -> update_cond h (Type (simple p))
- | Have p -> update_cond h (Have (simple p))
- | When p -> update_cond h (When (simple p))
- | Core p -> update_cond h (Core (simple p))
+ | State s -> update_cond h (State (Mstate.apply (equivalent_exp solvers) s))
+ | Init p -> update_cond h (Init (weaken p))
+ | Type p -> update_cond h (Type (weaken p))
+ | Have p -> update_cond h (Have (weaken p))
+ | When p -> update_cond h (When (weaken p))
+ | Core p -> update_cond h (Core (weaken p))
| Branch(p,_,_) -> List.iter (fun s -> s#target p) solvers; h
| Either _ -> h
let decide_branch modified solvers h =
match h.condition with
| Branch(p,a,b) ->
- let q = simplify_branch solvers p in
+ let q = equivalent_branch solvers p in
if q != p then
( modified := true ; update_cond h (Branch(q,a,b)) )
else h
@@ -939,7 +963,7 @@ let apply_simplifiers (solvers : simplifier list) (hs,g) =
List.iter (fun s -> s#fixpoint) solvers ;
let hs = List.map (decide_branch modified solvers) hs in
let hs = List.fold_right (add_infer modified) solvers hs in
- let p = simplify_goal solvers g in
+ let p = apply_goal solvers g in
if p != g || !modified then
Simplified (hs,p)
else
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index a2f02f254515b8036e078a1966612b9bb8cc827b..4a3f934474aa58370c7287b07ce8816cca658362 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -1067,10 +1067,10 @@ class type simplifier =
method fixpoint : unit
method infer : F.pred list
- method simplify_exp : F.term -> F.term
- method simplify_hyp : F.pred -> F.pred
- method simplify_branch : F.pred -> F.pred
- method simplify_goal : F.pred -> F.pred
+ method equivalent_exp : F.term -> F.term
+ method weaker_hyp : F.pred -> F.pred
+ method equivalent_branch : F.pred -> F.pred
+ method stronger_goal : F.pred -> F.pred
end
let is_atomic_pred = function
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 514110749b1f0336eb4f14377b20cd5e78ea32ec..ed9978d3a29740e35762419b90f09e44a4354bd9 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -576,16 +576,18 @@ class type simplifier =
method infer : F.pred list
(** Add new hypotheses implied by the original hypothesis. *)
- method simplify_exp : F.term -> F.term
- (** Currently simplify an expression. *)
- method simplify_hyp : F.pred -> F.pred
- (** Currently simplify an hypothesis before assuming it. In any
- case must return a weaker formula. *)
- method simplify_branch : F.pred -> F.pred
- (** Currently simplify a branch condition. In any case must return an
- equivalent formula. *)
- method simplify_goal : F.pred -> F.pred
- (** Simplify the goal. In any case must return a stronger formula. *)
+ method equivalent_exp : F.term -> F.term
+ (** Currently simplify an expression.
+ It must returns a equivalent formula from the assumed hypotheses. *)
+ method weaker_hyp : F.pred -> F.pred
+ (** Currently simplify an hypothesis before assuming it.
+ It must return a weaker formula from the assumed hypotheses. *)
+ method equivalent_branch : F.pred -> F.pred
+ (** Currently simplify a branch condition.
+ It must return an equivalent formula from the assumed hypotheses. *)
+ method stronger_goal : F.pred -> F.pred
+ (** Simplify the goal.
+ It must return a stronger formula from the assumed hypotheses. *)
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
index 06a4d869938de65e099b171b75d1b271aba60306..7b055f9626f0534549a3ffb75d39d3a6296d29fa 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
@@ -163,7 +163,7 @@ Goal Preservation of Invariant 'qed_ok' (file wp_behav.c, line 81):
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(n_1).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: n_1 <= 9.
(* Invariant 'qed_ok' *)
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index 4f4bf9be94af2fb141cb61287434873e95579349..8ee9e5fdf9b33fe732705bb05a771463647de355 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
@@ -18,14 +18,7 @@ Prove: true.
Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initialization of 'x2' (file wp_call_pre.c, line 26)
:
-Assume {
- Type: is_sint32(f) /\ is_sint32(x).
- (* Pre-condition 'Rd' *)
- Have: 0 <= x.
- (* Call 'f' *)
- Have: 0 < f.
-}
-Prove: (-1) <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
index 15d814ca6a84a699d2d2f8b7bafb37f6fb82eefd..63c5f1576f9bcce5d71cad71eb0588f4a083bb04 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
@@ -13,13 +13,6 @@ Prove: true.
Goal Instance of 'Pre-condition 'qed_ok,Rf' in 'f'' in 'double_call' at initialization of 'x2' (file wp_call_pre.c, line 26)
:
-Assume {
- Type: is_sint32(f) /\ is_sint32(x).
- (* Pre-condition 'Rd' *)
- Have: 0 <= x.
- (* Call 'f' *)
- Have: 0 < f.
-}
-Prove: (-1) <= x.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index ece0577112393b370922c68fdf7e52ab16d7c718..67664973b466ac756fd279aa63d3da5f437712eb 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -8,7 +8,7 @@
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_double_call_call_f_requires_qed_ok_Rf : Valid
-[wp] [Alt-Ergo] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
+[wp] [Qed] Goal typed_double_call_call_f_2_requires_qed_ok_Rf : Valid
[wp] [Qed] Goal typed_main_requires_qed_ok_Rmain : Valid
[wp] [Qed] Goal typed_main_ensures_qed_ok_Emain : Valid
[wp] [Qed] Goal typed_main_call_f_requires_qed_ok_Rf : Valid
@@ -17,11 +17,10 @@
[wp] [Qed] Goal typed_call_g_call_g_requires_qed_ok_Rga : Valid
[wp] [Qed] Goal typed_call_g_call_g_requires_Rgb : Valid
[wp] Proved goals: 9 / 9
- Qed: 8
- Alt-Ergo: 1
+ Qed: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- double_call 1 1 2 100%
+ double_call 2 - 2 100%
main 3 - 3 100%
call_main 2 - 2 100%
call_g 2 - 2 100%
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
index 9e0b53a7ea00e802ab646ce680706f403492eed3..745239a656b1bd3f1050de4cf623cbcce886bdba 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
@@ -158,13 +158,11 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'qed_ok,A1' (file arith.i, line 16):
-Assume { Type: is_uint8(i). }
-Prove: 0 <= i.
+Prove: true.
------------------------------------------------------------
Goal Assertion 'qed_ok,A2' (file arith.i, line 17):
-Assume { Type: is_uint8(i). (* Assertion 'qed_ok,A1' *) Have: 0 <= i. }
-Prove: i <= 255.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
index b8e9db163f8c7c8827d8cfad9f00adbc62f6f73f..aaf2d71df37874351849fd00cad82103468c01c0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_path.res.oracle
@@ -35,23 +35,7 @@ Prove: Mint_0[shift_sint32(b, i)] = v[i].
------------------------------------------------------------
Goal Preservation of Invariant (file assigns_path.i, line 16):
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: region(b.base) <= 0.
- (* Pre-condition *)
- Have: n <= 3.
- (* Invariant *)
- Have: 0 <= n.
- (* Invariant *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (Mint_0[shift_sint32(b, i_1)] = v[i_1]))).
- (* Then *)
- Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
index f06695c9f125f82f6b716b56813b8ea9009772d6..cb23d6906cfdf29fa29540c3642099871abb7a03 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/assigns_range.res.oracle
@@ -89,22 +89,7 @@ Prove: true.
Goal Instance of 'Pre-condition (file assigns_range.i, line 23) in 'assigns_t4_sup_bound'' in 'call_assigns_all' at call 'assigns_t4_sup_bound' (file assigns_range.i, line 40)
:
-Assume {
- Type: is_sint32(i) /\ is_sint32(j).
- (* Heap *)
- Type: IsArray_sint32(t2_0) /\ IsArray_sint32(t3_0).
- (* Pre-condition *)
- Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
- (* Call 'assigns_t1_an_element' *)
- Have: i <= 19.
- (* Call Effects *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((i_1 < i) \/ (j < i_1)) -> (t2_1[i_1] = t2_0[i_1])))).
- (* Call Effects *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 19) ->
- (((i_1 < i) \/ (20 <= i_1)) -> (t3_1[i_1] = t3_0[i_1])))).
-}
-Prove: 0 <= j.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -237,11 +222,6 @@ Prove: i <= 0.
Goal Instance of 'Pre-condition (file assigns_range.i, line 23) in 'assigns_t4_sup_bound'' in 'call_assigns_t4' at call 'assigns_t4_sup_bound' (file assigns_range.i, line 65)
:
-Assume {
- Type: is_sint32(i) /\ is_sint32(j).
- (* Pre-condition *)
- Have: (0 <= i) /\ (i <= j) /\ (j <= 19).
-}
-Prove: 0 <= j.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
index 17f0f3c5cb5a6b4af5b955af99c78f0a485efff9..6a44c5e64ba56925531942883fe890a7f127c378 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
@@ -112,7 +112,7 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (a <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (a <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 4c3b2575f9e95220d9b3b656cd14fa11ed3ed423..18d052e09ff36536fde976446a86f6b3e701e2bb 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
@@ -90,102 +90,7 @@ Prove: (a_16 = (1 + x[i])) /\ (a_17 = (1 + a_16)) /\ (a_18 = (1 + a_17)) /\
------------------------------------------------------------
Goal Preservation of Invariant (file chunk_typing.i, line 31):
-Let a = shift_uint64(u64_0, i).
-Let a_1 = shift_sint64(i64_0, i).
-Let a_2 = shift_uint32(u32_0, i).
-Let a_3 = shift_sint32(i32_0, i).
-Let a_4 = shift_uint16(u16_0, i).
-Let a_5 = shift_sint16(i16_0, i).
-Let a_6 = shift_uint8(u8_0, i).
-Let a_7 = shift_sint8(i8_0, i).
-Let a_8 = shift_uint64(u64_0, 0).
-Let a_9 = havoc(Mint_undef_5, Mint_5, a_8, 10).
-Let a_10 = shift_sint64(i64_0, 0).
-Let a_11 = havoc(Mint_undef_2, Mint_2, a_10, 10).
-Let a_12 = shift_uint32(u32_0, 0).
-Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
-Let a_14 = shift_sint32(i32_0, 0).
-Let a_15 = havoc(Mint_undef_1, Mint_1, a_14, 10).
-Let a_16 = shift_uint16(u16_0, 0).
-Let a_17 = havoc(Mint_undef_3, Mint_3, a_16, 10).
-Let a_18 = shift_sint16(i16_0, 0).
-Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
-Let a_20 = shift_uint8(u8_0, 0).
-Let a_21 = havoc(Mint_undef_6, Mint_6, a_20, 10).
-Let a_22 = shift_sint8(i8_0, 0).
-Let a_23 = havoc(Mchar_undef_0, Mchar_0, a_22, 10).
-Assume {
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
- is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
- is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
- is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
- is_sint32(1 + i) /\ is_sint16_chunk(a_19) /\ is_sint32_chunk(a_15) /\
- is_sint64_chunk(a_11) /\ is_sint8_chunk(a_23) /\
- is_uint16_chunk(a_17) /\ is_uint32_chunk(a_13) /\
- is_uint64_chunk(a_9) /\ is_uint8_chunk(a_21) /\
- is_sint16_chunk(a_19[a_5 <- 3]) /\ is_sint32_chunk(a_15[a_3 <- 5]) /\
- is_sint64_chunk(a_11[a_1 <- 7]) /\ is_sint8_chunk(a_23[a_7 <- 1]) /\
- is_uint16_chunk(a_17[a_4 <- 4]) /\ is_uint32_chunk(a_13[a_2 <- 6]) /\
- is_uint64_chunk(a_9[a <- 8]) /\ is_uint8_chunk(a_21[a_6 <- 2]).
- (* Heap *)
- Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
- (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
- (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
- (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
- linked(Malloc_0) /\ sconst(Mchar_0).
- (* Pre-condition *)
- Have: valid_rw(Malloc_0, a_18, 10) /\ valid_rw(Malloc_0, a_14, 10) /\
- valid_rw(Malloc_0, a_10, 10) /\ valid_rw(Malloc_0, a_22, 10) /\
- valid_rw(Malloc_0, a_16, 10) /\ valid_rw(Malloc_0, a_12, 10) /\
- valid_rw(Malloc_0, a_8, 10) /\ valid_rw(Malloc_0, a_20, 10).
- (* Invariant *)
- Have: (0 <= i) /\ (i <= 10).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_23[shift_sint8(i8_0, i_1)] = 1))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_21[shift_uint8(u8_0, i_1)] = 2))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_19[shift_sint16(i16_0, i_1)] = 3))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_17[shift_uint16(u16_0, i_1)] = 4))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_15[shift_sint32(i32_0, i_1)] = 5))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_13[shift_uint32(u32_0, i_1)] = 6))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_11[shift_sint64(i64_0, i_1)] = 7))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_9[shift_uint64(u64_0, i_1)] = 8))).
- (* Then *)
- Have: i <= 9.
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_7, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_6, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_5, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_4, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_3, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_2, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_1, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a, 1).
- (* Assertion 'rte,signed_overflow' *)
- Have: i <= 2147483646.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
@@ -1846,100 +1751,7 @@ Prove: valid_rw(Malloc_0, shift_uint64(u64_0, i), 1).
------------------------------------------------------------
Goal Assertion 'rte,signed_overflow' (file chunk_typing.i, line 44):
-Let a = shift_uint64(u64_0, i).
-Let a_1 = shift_sint64(i64_0, i).
-Let a_2 = shift_uint32(u32_0, i).
-Let a_3 = shift_sint32(i32_0, i).
-Let a_4 = shift_uint16(u16_0, i).
-Let a_5 = shift_sint16(i16_0, i).
-Let a_6 = shift_uint8(u8_0, i).
-Let a_7 = shift_sint8(i8_0, i).
-Let a_8 = shift_uint64(u64_0, 0).
-Let a_9 = havoc(Mint_undef_5, Mint_5, a_8, 10).
-Let a_10 = shift_sint64(i64_0, 0).
-Let a_11 = havoc(Mint_undef_2, Mint_2, a_10, 10).
-Let a_12 = shift_uint32(u32_0, 0).
-Let a_13 = havoc(Mint_undef_4, Mint_4, a_12, 10).
-Let a_14 = shift_sint32(i32_0, 0).
-Let a_15 = havoc(Mint_undef_1, Mint_1, a_14, 10).
-Let a_16 = shift_uint16(u16_0, 0).
-Let a_17 = havoc(Mint_undef_3, Mint_3, a_16, 10).
-Let a_18 = shift_sint16(i16_0, 0).
-Let a_19 = havoc(Mint_undef_0, Mint_0, a_18, 10).
-Let a_20 = shift_uint8(u8_0, 0).
-Let a_21 = havoc(Mint_undef_6, Mint_6, a_20, 10).
-Let a_22 = shift_sint8(i8_0, 0).
-Let a_23 = havoc(Mchar_undef_0, Mchar_0, a_22, 10).
-Assume {
- Type: is_sint16_chunk(Mint_0) /\ is_sint32_chunk(Mint_1) /\
- is_sint64_chunk(Mint_2) /\ is_sint8_chunk(Mchar_0) /\
- is_uint16_chunk(Mint_3) /\ is_uint32_chunk(Mint_4) /\
- is_uint64_chunk(Mint_5) /\ is_uint8_chunk(Mint_6) /\ is_sint32(i) /\
- is_sint16_chunk(a_19) /\ is_sint32_chunk(a_15) /\
- is_sint64_chunk(a_11) /\ is_sint8_chunk(a_23) /\
- is_uint16_chunk(a_17) /\ is_uint32_chunk(a_13) /\
- is_uint64_chunk(a_9) /\ is_uint8_chunk(a_21) /\
- is_sint16_chunk(a_19[a_5 <- 3]) /\ is_sint32_chunk(a_15[a_3 <- 5]) /\
- is_sint64_chunk(a_11[a_1 <- 7]) /\ is_sint8_chunk(a_23[a_7 <- 1]) /\
- is_uint16_chunk(a_17[a_4 <- 4]) /\ is_uint32_chunk(a_13[a_2 <- 6]) /\
- is_uint64_chunk(a_9[a <- 8]) /\ is_uint8_chunk(a_21[a_6 <- 2]).
- (* Heap *)
- Type: (region(i16_0.base) <= 0) /\ (region(i32_0.base) <= 0) /\
- (region(i64_0.base) <= 0) /\ (region(i8_0.base) <= 0) /\
- (region(u16_0.base) <= 0) /\ (region(u32_0.base) <= 0) /\
- (region(u64_0.base) <= 0) /\ (region(u8_0.base) <= 0) /\
- linked(Malloc_0) /\ sconst(Mchar_0).
- (* Pre-condition *)
- Have: valid_rw(Malloc_0, a_18, 10) /\ valid_rw(Malloc_0, a_14, 10) /\
- valid_rw(Malloc_0, a_10, 10) /\ valid_rw(Malloc_0, a_22, 10) /\
- valid_rw(Malloc_0, a_16, 10) /\ valid_rw(Malloc_0, a_12, 10) /\
- valid_rw(Malloc_0, a_8, 10) /\ valid_rw(Malloc_0, a_20, 10).
- (* Invariant *)
- Have: (0 <= i) /\ (i <= 10).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_23[shift_sint8(i8_0, i_1)] = 1))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_21[shift_uint8(u8_0, i_1)] = 2))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_19[shift_sint16(i16_0, i_1)] = 3))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_17[shift_uint16(u16_0, i_1)] = 4))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_15[shift_sint32(i32_0, i_1)] = 5))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_13[shift_uint32(u32_0, i_1)] = 6))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_11[shift_sint64(i64_0, i_1)] = 7))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_9[shift_uint64(u64_0, i_1)] = 8))).
- (* Then *)
- Have: i <= 9.
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_7, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_6, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_5, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_4, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_3, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_2, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a_1, 1).
- (* Assertion 'rte,mem_access' *)
- Have: valid_rw(Malloc_0, a, 1).
-}
-Prove: i <= 2147483646.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
index b97ad87904779045a6204e8e3bef96608684a346..bb59f39de147587a3ece2827d5e3c67c29a50f10 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/looplabels.res.oracle
@@ -35,30 +35,7 @@ Prove: P_IsEqual(havoc(Mint_undef_0, Mint_0, a_1, i), a, b, i).
------------------------------------------------------------
Goal Preservation of Invariant (file looplabels.i, line 18):
-Let a_1 = shift_sint32(b, 0).
-Let a_2 = shift_sint32(a, 0).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(Malloc_0).
- (* Pre-condition *)
- Have: 0 < n.
- (* Pre-condition *)
- Have: valid_rw(Malloc_0, a_2, n).
- (* Pre-condition *)
- Have: valid_rw(Malloc_0, a_1, n).
- (* Pre-condition *)
- Have: separated(a_2, n, a_1, n).
- (* Invariant *)
- Have: P_IsEqual(Mint_0, a, b, 0).
- (* Invariant *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant *)
- Have: P_IsEqual(havoc(Mint_undef_0, Mint_0, a_1, n), a, b, i).
- (* Then *)
- Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
index 45bac9e9756deeb47911d7acc0a215292a3d51fe..68a4d2e6a12bc598dda6c510b4900c096951b82a 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
@@ -145,16 +145,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file postassigns.c, line 38):
-Assume {
- Type: is_sint32(N) /\ is_sint32(i) /\ is_sint32(1 + i).
- (* Invariant *)
- Have: 0 <= N.
- (* Invariant *)
- Have: (i <= N) /\ (0 <= i).
- (* Then *)
- Have: i < N.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index b96c22a4802901437a86971598da3714e9176bf1..80262cbe5dcbc1b5163ee93464008fa7b0469d4d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
@@ -207,7 +207,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < size_0) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 < size_0).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
@@ -229,28 +229,7 @@ Prove: 0 < havoc(Mint_undef_0, Mint_0, a, i)[shift_sint32(t, i_1)].
------------------------------------------------------------
Goal Preservation of Invariant (file simpl_is_type.i, line 22):
-Let a = havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), size_0).
-Assume {
- Type: is_sint32(i) /\ is_sint32(size_0) /\ is_sint32(1 + i).
- (* Heap *)
- Type: region(t.base) <= 0.
- (* Pre-condition *)
- Have: 0 < size_0.
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < size_0) ->
- (Mint_0[shift_sint32(t, i_1)] < 0))).
- (* Invariant *)
- Have: (0 <= i) /\ (i <= size_0).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (0 < a[shift_sint32(t, i_1)]))).
- (* Invariant *)
- Have: forall i_1 : Z. ((i <= i_1) -> ((i_1 < size_0) ->
- (a[shift_sint32(t, i_1)] < 0))).
- (* Then *)
- Have: i < size_0.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
@@ -269,7 +248,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
@@ -308,7 +287,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (i_1 < size_0) /\ (i < i_1) /\ is_sint32(i_1).
+ When: (i_1 < size_0) /\ (i < i_1).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
@@ -340,7 +319,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i < size_0) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < size_0).
(* Pre-condition *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < size_0) ->
(Mint_0[shift_sint32(t, i_1)] < 0))).
@@ -422,25 +401,7 @@ Prove: exists i_1 : Z. (Mint_0[shift_sint32(t, i_1)] = x) /\ (0 <= i_1) /\
------------------------------------------------------------
Goal Preservation of Invariant (file simpl_is_type.i, line 44):
-Let x_1 = Mint_0[shift_sint32(t, i)].
-Assume {
- Type: is_sint32(i) /\ is_sint32(size_0) /\ is_sint32(x) /\
- is_sint32(1 + i) /\ is_sint32(x_1).
- (* Heap *)
- Type: region(t.base) <= 0.
- (* Pre-condition *)
- Have: 0 < size_0.
- (* Invariant *)
- Have: (0 <= i) /\ (i <= size_0).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (Mint_0[shift_sint32(t, i_1)] != x))).
- (* Then *)
- Have: i < size_0.
- (* Else *)
- Have: x_1 != x.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
@@ -457,7 +418,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i <= i_1) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= i_1).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
index 37df7d0a04ad853ae4c9a561b3f801830be8eeca..dc049f029f87f114c2375d65c23ae0278d5343d1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_variant_option.1.res.oracle
@@ -46,18 +46,7 @@ Prove: true.
------------------------------------------------------------
Goal Positivity of Loop variant at loop (file terminates_variant_option.i, line 41):
-Assume {
- Type: is_sint32(c1_0) /\ is_sint32(cpt_0) /\ is_sint32(cpt_0 - 1).
- (* Goal *)
- When: c1_0 != 0.
- (* Invariant *)
- Have: ((0 <= c1_0) -> ((cpt_0 <= c1_0) /\ (0 <= cpt_0))).
- (* Else *)
- Have: 2 <= cpt_0.
- (* Invariant *)
- Have: ((0 <= c1_0) -> (cpt_0 <= (1 + c1_0))).
-}
-Prove: 0 <= cpt_0.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
index cd6729ea2d5b979d9cf3e4b7439032f6a16aa32b..f444ed8fb1be46b98d9ba39559eabbf7004d6620 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
@@ -16,7 +16,7 @@ Let x_1 = lsr(x, 31).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i <= 30) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 30).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 1))), lsl(1, 1 + i)) != 0) <->
(land(x, lsl(1, i)) != 0).
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
index 6421bb6a22828470e479d8dd7c145274443ac35c..8fb1d6f4484ac63fd3a7988c1f3bc7c82edb7e35 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle
@@ -25,16 +25,16 @@
[wp] [Qed] Goal typed_lemma_ucN1_qed_ok : Valid
[wp] [Qed] Goal typed_lemma_ucN2_qed_ok : Valid
[wp] [Qed] Goal typed_cast_sgn_usgn_ensures_qed_ok_nat : Valid
-[wp] [Alt-Ergo] Goal typed_uchar_range_assert_qed_ok_A1 : Valid
-[wp] [Alt-Ergo] Goal typed_uchar_range_assert_qed_ok_A2 : Valid
+[wp] [Qed] Goal typed_uchar_range_assert_qed_ok_A1 : Valid
+[wp] [Qed] Goal typed_uchar_range_assert_qed_ok_A2 : Valid
[wp] Proved goals: 24 / 24
- Qed: 21
- Alt-Ergo: 3
+ Qed: 23
+ Alt-Ergo: 1
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma 20 1 21 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
cast_sgn_usgn 1 - 1 100%
- uchar_range - 2 2 100%
+ uchar_range 2 - 2 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
index 28b262760531731f5f26fbab84600533afb38420..825667eba07a3ab5731fe1d28aaf3489af749711 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle
@@ -5,7 +5,7 @@
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_job_ensures_N : Valid
[wp] [Alt-Ergo] Goal typed_job_ensures_A : Valid
-[wp] [Alt-Ergo] Goal typed_job_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_job_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_job_loop_invariant_2_established : Valid
@@ -13,11 +13,11 @@
[wp] [Qed] Goal typed_job_assigns_part1 : Valid
[wp] [Qed] Goal typed_job_assigns_part2 : Valid
[wp] Proved goals: 9 / 9
- Qed: 6
- Alt-Ergo: 3
+ Qed: 7
+ Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- job 6 3 9 100%
+ job 7 2 9 100%
------------------------------------------------------------
[wp] assigns_path.i:12: Warning:
Memory model hypotheses for function 'job':
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
index be1fcea95acc03cf80739f72f39b5459b1f1b573..a1167da627e2689310f2ec6a8663afd5eec4ea4c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle
@@ -16,17 +16,17 @@
[wp] [Alt-Ergo] Goal typed_call_assigns_all_call_assigns_t1_an_element_requires : Valid
[wp] [Qed] Goal typed_call_assigns_all_call_assigns_t2_bound_requires : Valid
[wp] [Qed] Goal typed_call_assigns_all_call_assigns_t3_inf_bound_requires : Valid
-[wp] [Alt-Ergo] Goal typed_call_assigns_all_call_assigns_t4_sup_bound_requires : Valid
+[wp] [Qed] Goal typed_call_assigns_all_call_assigns_t4_sup_bound_requires : Valid
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_call_assigns_t1_an_element_requires : Valid
[wp] [Alt-Ergo] Goal typed_call_assigns_t2_call_assigns_t2_bound_requires : Valid
-[wp] [Alt-Ergo] Goal typed_call_assigns_t4_call_assigns_t4_sup_bound_requires : Valid
+[wp] [Qed] Goal typed_call_assigns_t4_call_assigns_t4_sup_bound_requires : Valid
[wp] Proved goals: 17 / 17
- Qed: 12
- Alt-Ergo: 5
+ Qed: 14
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- call_assigns_all 12 2 14 100%
+ call_assigns_all 13 1 14 100%
call_assigns_t1 - 1 1 100%
call_assigns_t2 - 1 1 100%
- call_assigns_t4 - 1 1 100%
+ call_assigns_t4 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 98bcd99641039e586c9d25533d31f4c0c9f640af..de5777ff704aaf30b42ac5ddaa707c18f8fdc7cf 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -4,7 +4,7 @@
[rte:annot] annotating function function
[wp] 39 goals scheduled
[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_function_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_function_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_function_loop_invariant_2_established : Valid
@@ -30,7 +30,7 @@
[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_6 : Valid
[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_7 : Valid
[wp] [Alt-Ergo] Goal typed_function_assert_rte_mem_access_8 : Valid
-[wp] [Alt-Ergo] Goal typed_function_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_function_assert_rte_signed_overflow : Valid
[wp] [Qed] Goal typed_function_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_function_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_function_loop_assigns_part3 : Valid
@@ -43,11 +43,11 @@
[wp] [Qed] Goal typed_function_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_function_loop_variant_positive : Valid
[wp] Proved goals: 39 / 39
- Qed: 20
- Alt-Ergo: 19
+ Qed: 22
+ Alt-Ergo: 17
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- function 20 19 39 100%
+ function 22 17 39 100%
------------------------------------------------------------
[wp] chunk_typing.i:21: Warning:
Memory model hypotheses for function 'function':
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
index 3c5f14b5586a8915b0302faf8a82f7b3a8d4adb5..3882015f2cd0f3717f3c3638e0831ac0c20f7e49 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_copy_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_copy_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_copy_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_copy_loop_invariant_2_preserved : Valid
[wp] [Alt-Ergo] Goal typed_copy_loop_invariant_2_established : Valid
@@ -12,9 +12,9 @@
[wp] [Alt-Ergo] Goal typed_copy_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_copy_assigns : Valid
[wp] Proved goals: 8 / 8
- Qed: 3
- Alt-Ergo: 5
+ Qed: 4
+ Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- copy 3 5 8 100%
+ copy 4 4 8 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
index a6ade74dbc8fd0c2a59fd2339893c91f2b1c56c7..558c6e329de0c9193a491e6c1a4c9ce022116dc7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
@@ -23,7 +23,7 @@
[wp] [Alt-Ergo] Goal typed_job2_assigns_part7 : Valid
[wp] [Qed] Goal typed_job2_assigns_part8 : Valid
[wp] [Qed] Goal typed_job2_assigns_part9 : Valid
-[wp] [Alt-Ergo] Goal typed_job3_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job3_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_job3_loop_invariant_established : Valid
[wp] [Qed] Goal typed_job3_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_job3_loop_assigns_part2 : Valid
@@ -31,13 +31,13 @@
[wp] [Qed] Goal typed_job3_assigns_part1 : Valid
[wp] [Qed] Goal typed_job3_assigns_part2 : Valid
[wp] Proved goals: 27 / 27
- Qed: 23
- Alt-Ergo: 4
+ Qed: 24
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job1 10 - 10 100%
job2 8 2 10 100%
- job3 5 2 7 100%
+ job3 6 1 7 100%
------------------------------------------------------------
[wp] postassigns.c:7: Warning:
Memory model hypotheses for function 'job1':
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
index 64ff3d3d62f73f7e7ec8b87b02db286009cea7b1..ae73c30ff1306647c628e5ebf3015d4cea580dbd 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_f_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_f_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_f_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_f_loop_invariant_2_established : Valid
@@ -13,7 +13,7 @@
[wp] [Qed] Goal typed_f_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_f_loop_assigns_part2 : Valid
[wp] [Alt-Ergo] Goal typed_g_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_g_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_g_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_g_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_g_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_g_loop_invariant_2_established : Valid
@@ -22,11 +22,11 @@
[wp] [Alt-Ergo] Goal typed_check_acsl_check_ok_C2_absurd_is_cint : Valid
[wp] [Qed] Goal typed_check_acsl_check_ok_C5_absurd_cmp : Valid
[wp] Proved goals: 18 / 18
- Qed: 7
- Alt-Ergo: 11
+ Qed: 9
+ Alt-Ergo: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f 3 6 9 100%
- g 3 3 6 100%
+ f 4 5 9 100%
+ g 4 2 6 100%
check_acsl 1 2 3 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
index 4c690a7e344cdb7f48a22b1ea63cefb0207ccd58..192d6abde3bb1462937f389f3bea179af5177482 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_variant_option.1.res.oracle
@@ -24,7 +24,7 @@
[wp] [Qed] Goal typed_f1_loop_invariant_established : Valid
[wp] [Qed] Goal typed_f1_loop_assigns : Valid
[wp] [Qed] Goal typed_f1_loop_variant_decrease : Valid
-[wp] [Alt-Ergo] Goal typed_f1_loop_variant_positive : Valid
+[wp] [Qed] Goal typed_f1_loop_variant_positive : Valid
[wp] [Qed] Goal typed_trivial_variant_loop_assigns : Valid
[wp] [Qed] Goal typed_trivial_variant_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_trivial_variant_loop_variant_positive : Valid
@@ -32,13 +32,13 @@
[wp] [Qed] Goal typed_trivial_variant_default_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_trivial_variant_default_loop_variant_positive : Valid
[wp] Proved goals: 24 / 24
- Qed: 16
- Alt-Ergo: 4
+ Qed: 17
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
fails_positive 5 1 6 100%
fails_decreases 2 1 3 100%
- f1 3 2 5 100%
+ f1 4 1 5 100%
trivial_variant 3 - 3 100%
trivial_variant_default 3 - 3 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
index 5683dde8aeb75d334dfbcca8ca1510e3ecf372c6..214d5ef2e3c295a8a5ccb2a74c65b79b5f10d88a 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
@@ -7,8 +7,6 @@
------------------------------------------------------------
Goal Assertion (file bts779.i, line 6):
-Let x = Mint_0[shift_uint8(t, 0)].
-Assume { Type: is_uint8(x). (* Heap *) Type: region(t.base) <= 0. }
-Prove: x <= 255.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index 18231f2787cfacbce7f1fd426b27d0a7d6beaf6e..2e738afb004c169c4707afb644b505700e014741 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
@@ -7,18 +7,7 @@
------------------------------------------------------------
Goal Preservation of Invariant 'RANGE' (file issue_751.i, line 7):
-Let x = land(3840, R).
-Let x_1 = x / 256.
-Assume {
- Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j).
- (* Pre-condition *)
- Have: (0 < x) /\ (x <= 2303).
- (* Invariant 'RANGE' *)
- Have: (0 <= j) /\ (j <= x_1).
- (* Then *)
- Have: j < x_1.
-}
-Prove: (-1) <= j.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
index ca40bafd86e9470752fe7e8a3d7857e471e39c67..8faeff06e9fce75e58574e6da3390b8069df6522 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
@@ -3,12 +3,12 @@
[wp] Running WP plugin...
[rte:annot] annotating function f
[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_f_assert : Valid
+[wp] [Qed] Goal typed_f_assert : Valid
[wp] [Alt-Ergo] Goal typed_f_assert_rte_mem_access : Unsuccess
[wp] Proved goals: 1 / 2
- Qed: 0
- Alt-Ergo: 1 (unsuccess: 1)
+ Qed: 1
+ Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f - 1 2 50.0%
+ f 1 - 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
index 69f63c6e1c94ed8159119284c2bcf135b224b07b..6631c35af9b8fe108260f5e8018a3cd753ba75e1 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 40 goals scheduled
-[wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
+[wp] [Qed] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
[wp] [Qed] Goal typed_acquire_loop_invariant_RANGE_established : Valid
[wp] [Qed] Goal typed_acquire_loop_assigns_part1 : Valid
[wp] [Alt-Ergo] Goal typed_acquire_loop_assigns_part2 : Valid
@@ -44,10 +44,10 @@
[wp] [Alt-Ergo] Goal typed_issue_751_call_checks_4_requires_strict_pos_min : Valid
[wp] [Qed] Goal typed_issue_751_call_checks_4_requires_strict_neg_min : Valid
[wp] Proved goals: 40 / 40
- Qed: 26
- Alt-Ergo: 14
+ Qed: 27
+ Alt-Ergo: 13
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- acquire 2 2 4 100%
+ acquire 3 1 4 100%
issue_751 24 12 36 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index fda9d1592fcde0fd6bf80aa7a818d7c719d0c3e7..b91cab6038ff51321bd752683b5b40ceac3a8b64 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -14,18 +14,18 @@
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_2 : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_3 : Valid
+[wp] [Qed] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_3 : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_rte_unsigned_overflow_4 : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
+[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
[wp] Proved goals: 16 / 16
- Qed: 3
- Alt-Ergo: 13
+ Qed: 5
+ Alt-Ergo: 11
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 1 2 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- BinaryMultiplication 2 12 14 100%
+ BinaryMultiplication 4 10 14 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
index 2bbbd17af44cf460bbbc0b1e8d1139e9df2fbf38..a9679b500c90b55ba77f83446cce7da4423edf0c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
@@ -1,7 +1,7 @@
[ { "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 1 },
- "select": { "select": "inside-step", "at": 17, "kind": "have",
- "occur": 0, "target": "b_3 mod 2", "pattern": "%$b2" },
+ "select": { "select": "inside-step", "at": 18, "kind": "have",
+ "occur": 0, "target": "b_1 mod 2", "pattern": "%$b2" },
"children": { "Lower 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal",
@@ -10,52 +10,52 @@
"pattern": "to_uint64.2$x" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.9304,
+ "time": 5.0522,
"steps": 47 } ],
"Lower": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 5.6793,
+ "time": 4.8984,
"steps": 48 } ] } } ],
"Value 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
- "target": "(to_uint64 (a_1*b_1))",
+ "target": "(to_uint64 (a_1*b_3))",
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.3679,
- "steps": 184 } ],
+ "time": 5.0366,
+ "steps": 181 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 5.8854,
+ "time": 4.9686,
"steps": 42 } ],
"Upper": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.2747,
+ "time": 4.9181,
"steps": 42 } ] } } ],
"Value 1": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
- "target": "(to_uint64 (a_1*b_1))",
+ "target": "(to_uint64 (a_1*b_3))",
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.9832,
- "steps": 222 } ],
+ "time": 5.0078,
+ "steps": 218 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.0791,
+ "time": 4.7914,
"steps": 45 } ],
"Upper": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 5.1665,
+ "time": 4.8087,
"steps": 45 } ] } } ],
"Upper 1": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 6.0617,
+ "verdict": "valid", "time": 4.9897,
"steps": 48 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
index b6e73bdde324ab5d2f6961c6773b1b4b80656deb..a644fc380b73615879aa83975c72c77cc02b580a 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
@@ -13,7 +13,7 @@
[wp] [Alt-Ergo] Goal typed_binary_search_ensures_Result : Valid
[wp] [Qed] Goal typed_binary_search_ensures_Found : Valid
[wp] [Alt-Ergo] Goal typed_binary_search_ensures_NotFound : Valid
-[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_binary_search_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_binary_search_loop_invariant_Left_preserved : Valid
[wp] [Qed] Goal typed_binary_search_loop_invariant_Left_established : Valid
[wp] [Alt-Ergo] Goal typed_binary_search_loop_invariant_Range_preserved : Valid
@@ -32,9 +32,9 @@
[wp] [Alt-Ergo] Goal typed_binary_search_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_binary_search_loop_variant_positive : Valid
[wp] Proved goals: 28 / 28
- Qed: 7
- Alt-Ergo: 21
+ Qed: 8
+ Alt-Ergo: 20
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- binary_search 7 21 28 100%
+ binary_search 8 20 28 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
index 6fc4641c2a918d26bae446e524b503705425f3df..cf56af0792acf5251e177d957ad803686b349ad2 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
@@ -59,14 +59,14 @@
[rte:annot] annotating function iter_ptr
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_find_assert_rte_mem_access : Valid
-[wp] [Alt-Ergo] Goal typed_find_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_find_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_find_ptr_assert_rte_mem_access : Valid
[wp] Proved goals: 3 / 3
- Qed: 0
- Alt-Ergo: 3
+ Qed: 1
+ Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- find 7 11 18 100%
+ find 8 10 18 100%
find_ptr 6 12 18 100%
iter_ptr 2 6 8 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
index 472bae3aac8525769125b58c733be5e59855b4e9..e8de3999255b2d81ee037bb558174382548f45fc 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
@@ -23,15 +23,15 @@
[wp] Running WP plugin...
[rte:annot] annotating function exo1
[wp] 5 goals scheduled
-[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_exo1_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_mem_access_2 : Valid
-[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_signed_overflow_2 : Valid
-[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_signed_overflow_3 : Valid
+[wp] [Qed] Goal typed_exo1_assert_rte_signed_overflow_2 : Valid
+[wp] [Qed] Goal typed_exo1_assert_rte_signed_overflow_3 : Valid
[wp] Proved goals: 5 / 5
- Qed: 0
- Alt-Ergo: 5
+ Qed: 3
+ Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- exo1 6 9 15 100%
+ exo1 9 6 15 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
index 9fb7098252504e09573928fbe1ffe9c1284fd622..0a3bf5e9d5081c59065d653cc00f8fba3d38f026 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
@@ -5,7 +5,7 @@
[wp] 22 goals scheduled
[wp] [Alt-Ergo] Goal typed_max_subarray_ensures : Valid
[wp] [Alt-Ergo] Goal typed_max_subarray_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_max_subarray_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_max_subarray_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_max_subarray_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_max_subarray_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_max_subarray_loop_invariant_2_established : Valid
@@ -26,11 +26,11 @@
[wp] [Qed] Goal typed_max_subarray_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_max_subarray_loop_variant_positive : Valid
[wp] Proved goals: 22 / 22
- Qed: 12
- Alt-Ergo: 10
+ Qed: 13
+ Alt-Ergo: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- max_subarray 12 10 22 100%
+ max_subarray 13 9 22 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte:annot] annotating function max_subarray
@@ -41,5 +41,5 @@
Alt-Ergo: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- max_subarray 12 11 23 100%
+ max_subarray 13 10 23 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index dfc94d8a3943ced736b0721f08a7b01c3b7c69c7..815f3a1cb7facb792db414590628ca0f0cb565d5 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -6,11 +6,11 @@
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_2 : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_3 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_2_established : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_3_preserved : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_3_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_3_established : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_4_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_4_established : Valid
@@ -38,11 +38,11 @@
[wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_positive : Valid
[wp] Proved goals: 34 / 34
- Qed: 19
- Alt-Ergo: 15
+ Qed: 21
+ Alt-Ergo: 13
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- equal_elements 19 15 34 100%
+ equal_elements 21 13 34 100%
------------------------------------------------------------
[wp] frama_c_exo3_solved.old.c:73: Warning:
Memory model hypotheses for function 'equal_elements':
@@ -60,7 +60,7 @@
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_mem_access_3 : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_index_bound_3 : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_index_bound_4 : Valid
@@ -71,11 +71,11 @@
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_8 : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound_5 : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_signed_overflow_2 : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_signed_overflow_2 : Valid
[wp] Proved goals: 16 / 16
- Qed: 11
- Alt-Ergo: 5
+ Qed: 13
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- equal_elements 30 20 50 100%
+ equal_elements 34 16 50 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 4bf9ab318fb2b123882eaa5b3254c0e63fcf9f24..2830d7a72a4a46b3f80be4044c2a31941ee299d4 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -6,12 +6,12 @@
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_v1_good : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_v2_good : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_ensures_v1_v2_diff : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_set_at_0_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_set_at_0_established : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_set_at_1 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_bound_preserved : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_bound_preserved : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_invariant_bound_established : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_seen_sound1_preserved : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_loop_invariant_seen_sound1_established : Valid
@@ -39,11 +39,11 @@
[wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_ref_equal_elements_loop_variant_2_positive : Valid
[wp] Proved goals: 35 / 35
- Qed: 18
- Alt-Ergo: 17
+ Qed: 20
+ Alt-Ergo: 15
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- equal_elements 18 17 35 100%
+ equal_elements 20 15 35 100%
------------------------------------------------------------
[wp] frama_c_exo3_solved.old.v2.c:56: Warning:
Memory model hypotheses for function 'equal_elements':
@@ -61,7 +61,7 @@
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_mem_access_3 : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_index_bound_3 : Valid
[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_index_bound_4 : Valid
@@ -72,11 +72,11 @@
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_8 : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound_5 : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_ref_equal_elements_assert_rte_signed_overflow_2 : Valid
+[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_signed_overflow_2 : Valid
[wp] Proved goals: 16 / 16
- Qed: 11
- Alt-Ergo: 5
+ Qed: 13
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- equal_elements 29 22 51 100%
+ equal_elements 33 18 51 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
index 9ca1fbbad3e4eaf7c77acb2bd4fd7bed774c63e1..630af9b91980e457d5386befc31a56df8b51dc08 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
@@ -5,11 +5,11 @@
[wp] 26 goals scheduled
[wp] [Qed] Goal typed_pair_complete_has_pair_no_pair : Valid
[wp] [Qed] Goal typed_pair_disjoint_has_pair_no_pair : Valid
-[wp] [Alt-Ergo] Goal typed_pair_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_pair_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_pair_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_pair_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_pair_loop_invariant_2_established : Valid
-[wp] [Alt-Ergo] Goal typed_pair_loop_invariant_3_preserved : Valid
+[wp] [Qed] Goal typed_pair_loop_invariant_3_preserved : Valid
[wp] [Qed] Goal typed_pair_loop_invariant_3_established : Valid
[wp] [Alt-Ergo] Goal typed_pair_loop_invariant_4_preserved : Valid
[wp] [Alt-Ergo] Goal typed_pair_loop_invariant_4_established : Valid
@@ -30,28 +30,28 @@
[wp] [Alt-Ergo] Goal typed_pair_no_pair_ensures : Valid
[wp] [Alt-Ergo] Goal typed_pair_has_pair_ensures : Valid
[wp] Proved goals: 26 / 26
- Qed: 16
- Alt-Ergo: 10
+ Qed: 18
+ Alt-Ergo: 8
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- pair 16 10 26 100%
+ pair 18 8 26 100%
------------------------------------------------------------
[wp] Running WP plugin...
[rte:annot] annotating function pair
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_pair_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_pair_assert_rte_index_bound_2 : Valid
-[wp] [Alt-Ergo] Goal typed_pair_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_pair_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_pair_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_pair_assert_rte_index_bound_3 : Valid
[wp] [Alt-Ergo] Goal typed_pair_assert_rte_index_bound_4 : Valid
[wp] [Qed] Goal typed_pair_assert_rte_index_bound_5 : Valid
[wp] [Qed] Goal typed_pair_assert_rte_index_bound_6 : Valid
-[wp] [Alt-Ergo] Goal typed_pair_assert_rte_signed_overflow_2 : Valid
+[wp] [Qed] Goal typed_pair_assert_rte_signed_overflow_2 : Valid
[wp] Proved goals: 9 / 9
- Qed: 4
- Alt-Ergo: 5
+ Qed: 6
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- pair 20 15 35 100%
+ pair 24 11 35 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
index 13ce327181d2578f82c4d34b8708521ed3719056..8204ab6fa7850bb613a937f6dace22ade03d88ae 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
@@ -18,8 +18,7 @@ Prove: P_R(x, a).
------------------------------------------------------------
Goal Post-condition (file cint.i, line 30) in 'signed_downcast':
-Assume { Type: is_sint16(signed_downcast_0) /\ is_sint32(signed_downcast_0).
-}
+Assume { Type: is_sint16(signed_downcast_0). }
Prove: P_R(signed_downcast_0, signed_downcast_0).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index 977dad88e4b8bd65073c642151a2889636f5cdf4..ff49553d88311ef1563b0e947cde8ea45e6f6c20 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
@@ -13,24 +13,7 @@ Prove: (50 <= A) /\ (A <= 100).
------------------------------------------------------------
Goal Preservation of Invariant (file combined.c, line 29):
-Assume {
- Type: is_sint32(A) /\ is_sint32(i) /\ is_sint32(v) /\ is_sint32(1 + i).
- (* Heap *)
- Type: region(t.base) <= 0.
- (* Assertion *)
- Have: (50 <= A) /\ (A <= 100).
- (* Invariant *)
- Have: (0 <= i) /\ (i <= 50).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- P_P(havoc(Mint_undef_0, Mint_0, shift_sint32(t, 0), 50)
- [shift_sint32(t, i_1)]))).
- (* Then *)
- Have: i <= 49.
- (* Call 'f' *)
- Have: P_P(v).
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
index 45e2914bd4368a4294ef5d1f7d79ced28026b58c..5e9cbd10437bd13908135ea1710ece6d0ef94af0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/copy.res.oracle
@@ -72,32 +72,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file copy.i, line 10):
-Let a_1 = shift_sint32(a, 0).
-Let a_2 = havoc(Mint_undef_0, Mint_0, a_1, n).
-Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
- (* Pre-condition *)
- Have: separated(a_1, n, shift_sint32(b, 0), n).
- (* Invariant 'Range' *)
- Have: 0 <= n.
- (* Invariant 'Range' *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant 'Copy' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
- (* Then *)
- Have: i < n.
- (* Assertion 'A' *)
- Have: forall i_1 : Z. let a_4 = shift_sint32(a, i_1) in ((0 <= i_1) ->
- ((i_1 < i) -> (a_3[a_4] = a_2[a_4]))).
- (* Assertion 'B' *)
- Have: forall i_1 : Z. let a_4 = shift_sint32(b, i_1) in ((0 <= i_1) ->
- ((i_1 < i) -> (a_3[a_4] = a_2[a_4]))).
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
index b346927e4d3c79a87ddca0d6d4f7969962483b14..b35e3645528169c24136512ccd5b11a3779230c7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
@@ -16,7 +16,7 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (i_1 <= b) /\ (a <= i_1) /\ is_sint32(i_1).
+ When: (i_1 <= b) /\ (a <= i_1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
@@ -87,7 +87,7 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (a <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (a <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
index 2721d73c7500aabcf175de96f4a81508a0ad48ed..ed64f075c63c343af27c65f1a726533d26fc6e35 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
@@ -48,32 +48,7 @@ Prove: (forall i_2 : Z. ((0 <= i_2) -> ((i_2 < n) ->
------------------------------------------------------------
Goal Preservation of Invariant 'I' (file prenex.i, line 19):
-Assume {
- Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(m) /\ is_sint32(n) /\
- is_sint32(1 + i).
- (* Heap *)
- Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
- (* Invariant 'I' *)
- Have: 0 <= n.
- (* Invariant 'I' *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant 'PI' *)
- Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
- ((i_1 < m) ->
- (Mint_0[shift_sint32(p, i_2)] < Mint_0[shift_sint32(q, i_1)]))))).
- (* Then *)
- Have: i < n.
- (* Invariant 'J' *)
- Have: 0 <= m.
- (* Invariant 'J' *)
- Have: (0 <= j) /\ (j <= m).
- (* Invariant 'PJ' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) ->
- (Mint_0[shift_sint32(p, i)] < Mint_0[shift_sint32(q, i_1)]))).
- (* Else *)
- Have: m <= j.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
@@ -122,36 +97,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'J' (file prenex.i, line 28):
-Let x = Mint_0[shift_sint32(p, i)].
-Let x_1 = Mint_0[shift_sint32(q, j)].
-Assume {
- Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(m) /\ is_sint32(n) /\
- is_sint32(1 + j) /\ is_sint32(x) /\ is_sint32(x_1).
- (* Heap *)
- Type: (region(p.base) <= 0) /\ (region(q.base) <= 0).
- (* Invariant 'I' *)
- Have: 0 <= n.
- (* Invariant 'I' *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant 'PI' *)
- Have: forall i_2,i_1 : Z. ((0 <= i_2) -> ((i_2 < i) -> ((0 <= i_1) ->
- ((i_1 < m) ->
- (Mint_0[shift_sint32(p, i_2)] < Mint_0[shift_sint32(q, i_1)]))))).
- (* Then *)
- Have: i < n.
- (* Invariant 'J' *)
- Have: 0 <= m.
- (* Invariant 'J' *)
- Have: (0 <= j) /\ (j <= m).
- (* Invariant 'PJ' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < j) ->
- (x < Mint_0[shift_sint32(q, i_1)]))).
- (* Then *)
- Have: j < m.
- (* Else *)
- Have: x < x_1.
-}
-Prove: (-1) <= j.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
index 99192ce42a745e79c0ad5c0db4e0dc9abf038296..72cc29ecc9f80e0b3607e643e19a3db7d752e257 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/repeat.res.oracle
@@ -13,27 +13,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant (file repeat.c, line 61):
-Let a = L_sequence(calls_1).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: is_sint32(calls_0).
- (* Pre-condition *)
- Have: L_sequence(calls_0) = nil.
- (* Invariant *)
- Have: 0 <= n.
- (* Invariant *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant *)
- Have: ([ 1, 2 ] *^ i) = a.
- (* Then *)
- Have: i < n.
- (* Call 'f' *)
- Have: L_sequence(calls_2) = a ^ [ 1 ].
- (* Call 'g' *)
- Have: L_sequence(calls_3) = a ^ [ 1, 2 ].
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
@@ -148,29 +128,7 @@ Prove: (a *^ 1 + i) = a_2.
------------------------------------------------------------
Goal Preservation of Invariant (file repeat.c, line 81):
-Let a = ([ 1, 2 ] *^ i).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: is_sint32(calls_0).
- (* Pre-condition *)
- Have: L_sequence(calls_0) = nil.
- (* Call 'f' *)
- Have: L_sequence(calls_1) = [ 1 ].
- (* Invariant *)
- Have: 0 <= n.
- (* Invariant *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant *)
- Have: L_sequence(calls_2) = a ^ [ 1 ].
- (* Then *)
- Have: i < n.
- (* Call 'g' *)
- Have: L_sequence(calls_3) = a ^ [ 1, 2 ].
- (* Call 'f' *)
- Have: L_sequence(calls_4) = a ^ [ 1, 2, 1 ].
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
index fedcdb66fb660ab5c85989b6c35ce166281fa5ba..156a43c16d4f721dea573881f62418033adc87ea 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/sequence.res.oracle
@@ -39,30 +39,7 @@ Prove: nth(a_1, 1 + i) = z.
------------------------------------------------------------
Goal Preservation of Invariant 'ok,id_max' (file sequence.i, line 97):
-Let a = ([ y ] *^ i).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x) /\ is_sint32(y) /\
- is_sint32(1 + i).
- (* Heap *)
- Type: is_sint32(call_seq_0).
- (* Pre-condition *)
- Have: L_call_obs(call_seq_0) = nil.
- (* Call 'f' *)
- Have: L_call_obs(call_seq_1) = [ x ].
- (* Invariant 'ok,id_min' *)
- Have: 0 <= i.
- (* Invariant 'ok,id_max' *)
- Have: if (0 <= n) then (i <= n) else (i <= 0).
- (* Invariant 'ok,inv' *)
- Have: L_call_obs(call_seq_2) = [ x ] ^ a.
- (* Then *)
- Have: i < n.
- (* Call 'g' *)
- Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ y ].
- (* Invariant 'ok,id_min' *)
- Have: (-1) <= i.
-}
-Prove: 0 <= n.
+Prove: true.
------------------------------------------------------------
@@ -72,28 +49,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'ok,id_min' (file sequence.i, line 96):
-Let a = ([ y ] *^ i).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x) /\ is_sint32(y) /\
- is_sint32(1 + i).
- (* Heap *)
- Type: is_sint32(call_seq_0).
- (* Pre-condition *)
- Have: L_call_obs(call_seq_0) = nil.
- (* Call 'f' *)
- Have: L_call_obs(call_seq_1) = [ x ].
- (* Invariant 'ok,id_min' *)
- Have: 0 <= i.
- (* Invariant 'ok,id_max' *)
- Have: if (0 <= n) then (i <= n) else (i <= 0).
- (* Invariant 'ok,inv' *)
- Have: L_call_obs(call_seq_2) = [ x ] ^ a.
- (* Then *)
- Have: i < n.
- (* Call 'g' *)
- Have: L_call_obs(call_seq_3) = [ x ] ^ a ^ [ y ].
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
index c1383873535e632ba413a93d587aa48bb2c3a20d..faadd1df8084289a61a9d27e3c3bfd6d055fb10a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/string_c.res.oracle
@@ -66,19 +66,7 @@ Prove: to_uint64(1 + i) <= n.
------------------------------------------------------------
Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 33):
-Assume {
- Type: is_uint64(n).
- (* Heap *)
- Type: (region(dest_0.base) <= 0) /\ (region(src_0.base) <= 0) /\
- linked(Malloc_0).
- (* Pre-condition 'valid_dest' *)
- Have: P_valid_or_empty(Malloc_0, dest_0, n).
- (* Pre-condition 'valid_src' *)
- Have: P_valid_read_or_empty(Malloc_0, src_0, n).
- (* Pre-condition 'separation' *)
- Have: separated(shift_sint8(dest_0, 0), n, shift_sint8(src_0, 0), n).
-}
-Prove: 0 <= n.
+Prove: true.
------------------------------------------------------------
@@ -338,28 +326,7 @@ Prove: to_uint64(1 + i) <= n.
------------------------------------------------------------
Goal Establishment of Invariant 'no_eva' (file FRAMAC_SHARE/libc/string.c, line 95):
-Let a = shift_sint8(d, 0).
-Let a_1 = shift_sint8(s, 0).
-Assume {
- Type: is_sint32(memoverlap_0) /\ is_uint64(n).
- (* Heap *)
- Type: (region(d.base) <= 0) /\ (region(s.base) <= 0) /\ linked(Malloc_0).
- (* Pre-condition 'valid_dest' *)
- Have: P_valid_or_empty(Malloc_0, d, n).
- (* Pre-condition 'valid_src' *)
- Have: P_valid_read_or_empty(Malloc_0, s, n).
- (* Else *)
- Have: n != 0.
- (* Call 'memoverlap' *)
- Have: ((separated(a, n, a_1, n) -> (memoverlap_0 = 0))) /\
- ((addr_le(d, s) -> (addr_lt(s, shift_sint8(d, n)) ->
- ((!separated(a, n, a_1, n)) -> (memoverlap_0 = (-1)))))) /\
- ((addr_lt(s, d) -> (addr_le(d, shift_sint8(s, n)) ->
- ((!separated(a, n, a_1, n)) -> (memoverlap_0 = 1))))).
- (* Then *)
- Have: memoverlap_0 <= 0.
-}
-Prove: 0 <= n.
+Prove: true.
------------------------------------------------------------
@@ -850,48 +817,7 @@ Prove: true.
Goal Assigns (file FRAMAC_SHARE/libc/string.h, line 122) in 'memmove' (6/7):
Effect at line 115
-Let a = shift_sint8(d, 0).
-Let a_1 = havoc(Mchar_undef_0, Mchar_0, a, n).
-Let x = to_uint64(n - 1).
-Let a_2 = shift_sint8(src_0, 0).
-Assume {
- Type: is_sint32(memoverlap_0) /\ is_uint64(i) /\ is_uint64(n).
- (* Heap *)
- Type: (region(d.base) <= 0) /\ (region(src_0.base) <= 0) /\
- linked(Malloc_0) /\ sconst(Mchar_0).
- (* Goal *)
- When: !invalid(Malloc_0, a, 1).
- (* Pre-condition 'valid_dest' *)
- Have: P_valid_or_empty(Malloc_0, d, n).
- (* Pre-condition 'valid_src' *)
- Have: P_valid_read_or_empty(Malloc_0, src_0, n).
- (* Else *)
- Have: n != 0.
- (* Call 'memoverlap' *)
- Have: ((separated(a, n, a_2, n) -> (memoverlap_0 = 0))) /\
- ((addr_le(d, src_0) -> (addr_lt(src_0, shift_sint8(d, n)) ->
- ((!separated(a, n, a_2, n)) -> (memoverlap_0 = (-1)))))) /\
- ((addr_lt(src_0, d) -> (addr_le(d, shift_sint8(src_0, n)) ->
- ((!separated(a, n, a_2, n)) -> (memoverlap_0 = 1))))).
- (* Else *)
- Have: 0 < memoverlap_0.
- (* Invariant 'no_eva' *)
- Have: x < n.
- (* Invariant 'no_eva' *)
- Have: forall i_1 : Z. ((i_1 < n) -> ((x < i_1) ->
- (Mchar_0[shift_sint8(src_0, i_1)] = Mchar_0[shift_sint8(d, i_1)]))).
- (* Invariant 'no_eva' *)
- Have: (0 <= i) /\ (i < n).
- (* Invariant 'no_eva' *)
- Have: forall i_1 : Z. ((i < i_1) -> ((i_1 < n) ->
- (a_1[shift_sint8(d, i_1)] = Mchar_0[shift_sint8(src_0, i_1)]))).
- (* Invariant 'no_eva' *)
- Have: forall i_1 : Z. let a_3 = shift_sint8(src_0, i_1) in ((i_1 <= i) ->
- ((0 <= i_1) -> (a_1[a_3] = Mchar_0[a_3]))).
- (* Else *)
- Have: i <= 0.
-}
-Prove: 0 < n.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
index c1f541d00af218c3a2c837305606b0681f1e9f7d..ce1db3baf849bcda6d5c7bc45ce2fad9d913cc87 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
@@ -4,5 +4,5 @@
"pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
"Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0263,
+ "verdict": "valid", "time": 0.0174,
"steps": 32 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
index 95cf3e5f2953bc7ed7b6c9ad5939b20299677781..6efc632858bf4117e91e9c9f8cb43ca24a57fcc7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
@@ -3,6 +3,6 @@
"target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0129,
+ "verdict": "valid", "time": 0.0166,
"steps": 32 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
index e0dfdd314121b4941bfe645786d7f0b45dcbc541..6b924bddcb43114d07f388f2208f5d07fcf42fa1 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle
@@ -6,7 +6,7 @@
[wp] [Alt-Ergo] Goal typed_copy_ensures : Valid
[wp] [Alt-Ergo] Goal typed_copy_loop_invariant_Copy_preserved : Valid
[wp] [Qed] Goal typed_copy_loop_invariant_Copy_established : Valid
-[wp] [Alt-Ergo] Goal typed_copy_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_copy_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_copy_loop_invariant_Range_established : Valid
[wp] [Alt-Ergo] Goal typed_copy_assert_A : Valid
[wp] [Alt-Ergo] Goal typed_copy_assert_B : Valid
@@ -15,9 +15,9 @@
[wp] [Alt-Ergo] Goal typed_copy_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_copy_assigns : Valid
[wp] Proved goals: 11 / 11
- Qed: 5
- Alt-Ergo: 6
+ Qed: 6
+ Alt-Ergo: 5
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- copy 5 6 11 100%
+ copy 6 5 11 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
index 2e2b36878d3e5f9274b92febfa5d9a2927f042f6..02ab35a20338ee218e2719fb9c411bb64d052a3b 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle
@@ -4,11 +4,11 @@
[wp] Warning: Missing RTE guards
[wp] 12 goals scheduled
[wp] [Alt-Ergo] Goal typed_diag_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_diag_loop_invariant_I_preserved : Valid
+[wp] [Qed] Goal typed_diag_loop_invariant_I_preserved : Valid
[wp] [Qed] Goal typed_diag_loop_invariant_I_established : Valid
[wp] [Alt-Ergo] Goal typed_diag_loop_invariant_PI_preserved : Valid
[wp] [Qed] Goal typed_diag_loop_invariant_PI_established : Valid
-[wp] [Alt-Ergo] Goal typed_diag_loop_invariant_J_preserved : Valid
+[wp] [Qed] Goal typed_diag_loop_invariant_J_preserved : Valid
[wp] [Qed] Goal typed_diag_loop_invariant_J_established : Valid
[wp] [Alt-Ergo] Goal typed_diag_loop_invariant_PJ_preserved : Valid
[wp] [Qed] Goal typed_diag_loop_invariant_PJ_established : Valid
@@ -16,9 +16,9 @@
[wp] [Qed] Goal typed_diag_loop_assigns_part2 : Valid
[wp] [Qed] Goal typed_diag_loop_assigns_2 : Valid
[wp] Proved goals: 12 / 12
- Qed: 7
- Alt-Ergo: 5
+ Qed: 9
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- diag 7 5 12 100%
+ diag 9 3 12 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
index 9efba93bde83103ce06ccbb72bb4a49d1d0b2276..53ead599403a2c8c4c8df1443698a2d5ae2f49f9 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle
@@ -33,7 +33,7 @@
[wp] [Qed] Goal typed_unroll_assigns_normal_part10 : Valid
[wp] [Qed] Goal typed_unroll_assigns_normal_part11 : Valid
[wp] [Qed] Goal typed_induction_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_induction_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_induction_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_induction_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_induction_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_induction_loop_invariant_2_established : Valid
@@ -42,7 +42,7 @@
[wp] [Qed] Goal typed_induction_assigns_exit_part2 : Valid
[wp] [Qed] Goal typed_induction_assigns_normal : Valid
[wp] [Alt-Ergo] Goal typed_shifted_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_shifted_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_shifted_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_shifted_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_shifted_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_shifted_loop_invariant_2_established : Valid
@@ -52,12 +52,12 @@
[wp] [Qed] Goal typed_shifted_assigns_normal_part1 : Valid
[wp] [Qed] Goal typed_shifted_assigns_normal_part2 : Valid
[wp] Proved goals: 47 / 47
- Qed: 42
- Alt-Ergo: 5
+ Qed: 44
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
master 3 - 3 100%
unroll 25 - 25 100%
- induction 7 2 9 100%
- shifted 7 3 10 100%
+ induction 8 1 9 100%
+ shifted 8 2 10 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
index 7602867d0780d45feb0ba2978880f36079220b2c..890caa285aa06ad4e13d7fa980f2477be2202a36 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle
@@ -25,9 +25,9 @@
[wp] [Alt-Ergo] Goal typed_caveat_sequence_g_not_called_ensures_ok_q3 : Valid
[wp] [Qed] Goal typed_caveat_loops_ensures_ok_first : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_ensures_ok_last : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_loop_invariant_ok_id_max_preserved : Valid
+[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_max_preserved : Valid
[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_max_established : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_loop_invariant_ok_id_min_preserved : Valid
+[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_min_preserved : Valid
[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_min_established : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_loop_invariant_ok_inv_preserved : Valid
[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_inv_established : Valid
@@ -43,11 +43,11 @@
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v1 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v2 : Valid
[wp] Proved goals: 39 / 39
- Qed: 26
- Alt-Ergo: 13
+ Qed: 28
+ Alt-Ergo: 11
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
no_calls 5 5 10 100%
sequence 8 2 10 100%
- loops 13 6 19 100%
+ loops 15 4 19 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
index fb728b9fa94a45d92d1f3cf5d409d84160adeadd..8c504062e5a4b190e871f43e23f3c5fe64cd5410 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle
@@ -20,9 +20,9 @@
[wp] [Alt-Ergo] Goal typed_caveat_sequence_g_not_called_ensures_ok_q3 : Valid
[wp] [Qed] Goal typed_caveat_loops_ensures_ok_first : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_ensures_ok_last : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_loop_invariant_ok_id_max_preserved : Valid
+[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_max_preserved : Valid
[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_max_established : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_loops_loop_invariant_ok_id_min_preserved : Valid
+[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_min_preserved : Valid
[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_id_min_established : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_loop_invariant_ok_inv_preserved : Valid
[wp] [Qed] Goal typed_caveat_loops_loop_invariant_ok_inv_established : Valid
@@ -38,11 +38,11 @@
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v1 : Valid
[wp] [Alt-Ergo] Goal typed_caveat_loops_g_not_called_ensures_ok_v2 : Valid
[wp] Proved goals: 34 / 34
- Qed: 23
- Alt-Ergo: 11
+ Qed: 25
+ Alt-Ergo: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
no_calls 2 3 5 100%
sequence 8 2 10 100%
- loops 13 6 19 100%
+ loops 15 4 19 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
index cc9031fcb59f098af6fb1aa7717aa675b908d1cc..3d41a25d9572f1c6917dbe8d66df9426920c3ccb 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle
@@ -6,7 +6,7 @@
[wp] [Alt-Ergo] Goal typed_memcpy_ensures_copied_contents : Valid
[wp] [Qed] Goal typed_memcpy_ensures_result_ptr : Valid
[wp] [Alt-Ergo] Goal typed_memcpy_loop_invariant_no_eva_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_memcpy_loop_invariant_no_eva_established : Valid
+[wp] [Qed] Goal typed_memcpy_loop_invariant_no_eva_established : Valid
[wp] [Alt-Ergo] Goal typed_memcpy_loop_invariant_no_eva_2_preserved : Valid
[wp] [Qed] Goal typed_memcpy_loop_invariant_no_eva_2_established : Valid
[wp] [Qed] Goal typed_memcpy_loop_assigns_part1 : Valid
@@ -18,7 +18,7 @@
[wp] [Alt-Ergo] Goal typed_memmove_ensures_copied_contents : Valid
[wp] [Qed] Goal typed_memmove_ensures_result_ptr : Valid
[wp] [Alt-Ergo] Goal typed_memmove_loop_invariant_no_eva_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_memmove_loop_invariant_no_eva_established : Valid
+[wp] [Qed] Goal typed_memmove_loop_invariant_no_eva_established : Valid
[wp] [Alt-Ergo] Goal typed_memmove_loop_invariant_no_eva_2_preserved : Valid
[wp] [Qed] Goal typed_memmove_loop_invariant_no_eva_2_established : Valid
[wp] [Alt-Ergo] Goal typed_memmove_loop_invariant_no_eva_3_preserved : Valid
@@ -41,17 +41,17 @@
[wp] [Qed] Goal typed_memmove_assigns_normal_part3 : Valid
[wp] [Qed] Goal typed_memmove_assigns_normal_part4 : Valid
[wp] [Qed] Goal typed_memmove_assigns_normal_part5 : Valid
-[wp] [Alt-Ergo] Goal typed_memmove_assigns_normal_part6 : Valid
+[wp] [Qed] Goal typed_memmove_assigns_normal_part6 : Valid
[wp] [Qed] Goal typed_memmove_assigns_normal_part7 : Valid
[wp] [Alt-Ergo] Goal typed_memmove_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_memmove_loop_variant_positive : Valid
[wp] [Alt-Ergo] Goal typed_memmove_loop_variant_2_decrease : Valid
[wp] [Qed] Goal typed_memmove_loop_variant_2_positive : Valid
[wp] Proved goals: 44 / 44
- Qed: 23
- Alt-Ergo: 21
+ Qed: 26
+ Alt-Ergo: 18
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- memcpy 6 6 12 100%
- memmove 17 15 32 100%
+ memcpy 7 5 12 100%
+ memmove 19 13 32 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
index 1c97c0efd6fc200100d43ffe2b726792238d7235..fee182f4fb27d5d514f2a00bb1ea971d893a4636 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
@@ -1,6 +1,6 @@
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
- "target": "(P_zeroed\n Mint_37[(shift_uint32 t_2 0)->0][(shift_uint32 t_2 1)->0]\n [(shift_uint32 t_2 2)->0][(shift_uint32 t_2 3)->0][(shift_uint32 t_2 4)\n ->0][(shift_uint32 t_2 5)->0][(shift_uint32 t_2 6)->0]\n [(shift_uint32 t_2 7)->0][(shift_uint32 t_2 8)->0][(shift_uint32 t_2 9)\n ->0][(shift_uint32 t_2 10)->0][(shift_uint32 t_2 11)->0]\n [(shift_uint32 t_2 12)->0][(shift_uint32 t_2 13)->0]\n [(shift_uint32 t_2 14)->0][(shift_uint32 t_2 15)->0] t_2 0 15)",
+ "target": "(P_zeroed\n Mint_37[(shift_uint32 t_0 0)->0][(shift_uint32 t_0 1)->0]\n [(shift_uint32 t_0 2)->0][(shift_uint32 t_0 3)->0][(shift_uint32 t_0 4)\n ->0][(shift_uint32 t_0 5)->0][(shift_uint32 t_0 6)->0]\n [(shift_uint32 t_0 7)->0][(shift_uint32 t_0 8)->0][(shift_uint32 t_0 9)\n ->0][(shift_uint32 t_0 10)->0][(shift_uint32 t_0 11)->0]\n [(shift_uint32 t_0 12)->0][(shift_uint32 t_0 13)->0]\n [(shift_uint32 t_0 14)->0][(shift_uint32 t_0 15)->0] t_0 0 15)",
"pattern": "P_zeroed[=]$t015[=]shift_uint320" },
"children": { "Unfold 'P_zeroed'": [ { "header": "Range",
"tactic": "Wp.range",
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
index dd1cd3edf7d9ef503650337d4d5bca8a6a5e038f..b65abf98b7fcfae08fcaf1c97159d599c8c10f3e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
@@ -14,6 +14,7 @@
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
@@ -30,30 +31,13 @@
Prove: true.
Prover Qed returns Valid
- ------------------------------------------------------------
-[wp:script:allgoals]
- typed_check_lemma_and_modulo_us_255 subgoal:
-
- Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
- Assume { Have: is_uint16(us_0). }
- Prove: 0 <= us_0.
-
- ------------------------------------------------------------
-[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
-[wp:script:allgoals]
- typed_check_lemma_and_modulo_us_255 subgoal:
-
- Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
- Prove: true.
- Prover Qed returns Valid
-
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
- Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
- Prove: 0 <= us_0.
+ Prove: true.
+ Prover Qed returns Valid
------------------------------------------------------------
[wp:script:allgoals]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
index e40e8863e3cf66cd9c1c3c6e4d1f0fa5d083d726..84b0af02539d9a89a4563ba38a73f7273b5d79b0 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_u.json
@@ -8,7 +8,9 @@
"select": { "select": "clause-goal",
"target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
"pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
- "children": { "Goal 1/3": [ { "header": "Definition",
+ "children": { "Goal 1/3": [ { "prover": "qed",
+ "verdict": "valid" },
+ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
index 0232433c576b0cb20e7c6108b28bec094abaa799..67fe782ea8a713724aaa08a6bd0215e2afe57bbf 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.session/script/check_lemma_and_modulo_us_255.json
@@ -2,7 +2,8 @@
"params": { "Wp.modmask.revert": false },
"select": { "select": "inside-goal", "occur": 0,
"target": "us_0 mod 256", "pattern": "%$us256" },
- "children": { "Mask Guard": [ { "header": "Definition",
+ "children": { "Mask Guard": [ { "prover": "qed", "verdict": "valid" },
+ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
index dd1cd3edf7d9ef503650337d4d5bca8a6a5e038f..b65abf98b7fcfae08fcaf1c97159d599c8c10f3e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.res.oracle
@@ -14,6 +14,7 @@
Prove: (is_uint16 us_0) -> ((us_0 mod 256)=(land 255 us_0))
------------------------------------------------------------
+[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
@@ -30,30 +31,13 @@
Prove: true.
Prover Qed returns Valid
- ------------------------------------------------------------
-[wp:script:allgoals]
- typed_check_lemma_and_modulo_us_255 subgoal:
-
- Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-0 (generated):
- Assume { Have: is_uint16(us_0). }
- Prove: 0 <= us_0.
-
- ------------------------------------------------------------
-[wp] [Script] Goal typed_check_lemma_and_modulo_us_255 : Valid
-[wp:script:allgoals]
- typed_check_lemma_and_modulo_us_255 subgoal:
-
- Goal Wp.Tactical.typed_check_lemma_and_modulo_us_255-1 (generated):
- Prove: true.
- Prover Qed returns Valid
-
------------------------------------------------------------
[wp:script:allgoals]
typed_check_lemma_and_modulo_u subgoal:
Goal Wp.Tactical.typed_check_lemma_and_modulo_u-2 (generated):
- Assume { Have: 0 <= shift_0. Have: shift_0 <= 31. Have: is_uint32(us_0). }
- Prove: 0 <= us_0.
+ Prove: true.
+ Prover Qed returns Valid
------------------------------------------------------------
[wp:script:allgoals]
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
index 7d2e4b041e8f70d94528bc04cf06fc7d49bbbb6e..51fbe949924301501fb2a9aa26320303e520adaf 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_u.json
@@ -8,7 +8,9 @@
"select": { "select": "clause-goal",
"target": "let x_0 = (lsl 1 shift_0) in\n(0<=us_0) /\\ (0<x_0) /\\ (exists i_0:int.\n ((lsl 1 i_0)=x_0) /\\ (0<=i_0))",
"pattern": "&<=<\\E0$us0lsl1$shiftlsl011$shift" },
- "children": { "Goal 1/3": [ { "header": "Definition",
+ "children": { "Goal 1/3": [ { "prover": "qed",
+ "verdict": "valid" },
+ { "header": "Definition",
"tactic": "Wp.unfold",
"params": {},
"select":
diff --git a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
index a56490bac7af0b6011890ef00ef38f25fa4cd251..c16388ade5d0163bb875e3e7640aa57f4b96b603 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
+++ b/src/plugins/wp/tests/wp_tip/oracle/modmask.1.session/script/check_lemma_and_modulo_us_255.json
@@ -2,7 +2,8 @@
"params": { "Wp.modmask.revert": false },
"select": { "select": "inside-goal", "occur": 0,
"target": "(land 255 us_0)", "pattern": "land255$us" },
- "children": { "Mod Guard": [ { "header": "Definition",
+ "children": { "Mod Guard": [ { "prover": "qed", "verdict": "valid" },
+ { "header": "Definition",
"tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-step",
"at": 0, "kind": "have",
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
index 2a359dbab3ad22d87d88d11534edd84db6f4497e..77a4f51c832cb8e9d049e59dd20d0b4644788ff9 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
@@ -3,10 +3,10 @@
"select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
"pattern": "L_f$x" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
- "time": 0.0047, "steps": 6 } ],
+ "time": 0.0074, "steps": 6 } ],
"Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0041,
+ "verdict": "valid", "time": 0.0098,
"steps": 21 } ],
"Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0054,
+ "verdict": "valid", "time": 0.0097,
"steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
index 9ca995ee6234769c156b30223f2b7d8dcb67e964..255539ba9f34b22d89852d5659ffc0969380c9f1 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
@@ -5,7 +5,7 @@
"verdict": "valid", "time": 0.0094,
"steps": 25 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0238,
+ "verdict": "valid", "time": 0.0157,
"steps": 53 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
index b07a89798751525300ec38be4ef5de65ee73b4cb..97c383396b0c68dc8ea302b5db23e1fe35c93227 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
@@ -5,7 +5,7 @@
"verdict": "valid", "time": 0.0098,
"steps": 25 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0248,
+ "verdict": "valid", "time": 0.0198,
"steps": 54 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
index 885feb947bdb3b276a90fc8d54f807ae6dd76e79..cadd5e501016b03034d1b6c4b5778d254468abcd 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid" },
- { "header": "Sequence", "tactic": "Wp.sequence",
+[ { "header": "Sequence", "tactic": "Wp.sequence",
"params": { "seq.side": "left" },
"select": { "select": "inside-goal", "occur": 0,
"target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
index 75e4064cdb6eb792772488a295e01855174a6132..2c6b678d138d5ffc43f3394c72fe508f44b8b8ec 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid" },
- { "header": "Sequence", "tactic": "Wp.sequence",
+[ { "header": "Sequence", "tactic": "Wp.sequence",
"params": { "seq.side": "right" },
"select": { "select": "inside-goal", "occur": 0,
"target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
index 65a87aa59ca69040135319b35d107a49d773886a..60f8f7acd6cea516bf05aa93a1b4cdc243f49e83 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid" },
- { "header": "Sequence", "tactic": "Wp.sequence",
+[ { "header": "Sequence", "tactic": "Wp.sequence",
"params": { "seq.side": "sum" },
"select": { "select": "inside-goal", "occur": 0,
"target": "(repeat a_0 (p_0+q_0))",
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
index 207e9befdb79fe21441383cf88a6bebadced293d..91d993407e90198cfac7642dd37c622a3ba79925 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -64,7 +64,7 @@ Goal Post-condition (file cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
Assume {
- Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
+ Type: is_sint8(x) /\ is_sint8(x_1).
(* Heap *)
Type: (region(p.base) <= 0) /\ sconst(Mchar_0).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
index f456415436e1c7639e50fead09a66a353db816f1..76f3b9532f3c8ba5cf43aac5657b1af1bfd9d1c9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -64,7 +64,7 @@ Goal Post-condition (file cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
Assume {
- Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
+ Type: is_sint8(x) /\ is_sint8(x_1).
(* Heap *)
Type: (region(p.base) <= 0) /\ sconst(Mchar_0).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
index 3161feeff647794efb090e0c7c0f7395ff304a68..652ab955538806f8246c98cc19cc31858a25b954 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
@@ -31,7 +31,7 @@ Assume {
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i <= 9) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 9).
(* Pre-condition *)
Have: P_inv(Mint_0, p).
(* Assertion *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
index 67d2f08869b917c50e09654bbfbf7710c24b16eb..62c3c4fdabf0c30991d0dc18e9945ba998b981aa 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
@@ -31,7 +31,7 @@ Assume {
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i <= 9) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 9).
(* Pre-condition *)
Have: P_inv(Mint_0, p).
(* Assertion *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
index 7088dae230bb076c156e35ba64b86218710ae268..81b6a3c63eaa995bcb9d50e5a03e1cff6e779fd4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
@@ -9,13 +9,6 @@
------------------------------------------------------------
Goal Assertion (file unit_call.i, line 14):
-Assume {
- Type: is_sint32(r_1) /\ is_sint32(r).
- (* Call 'f' *)
- Have: r < 0.
- (* Call 'f' *)
- Have: 0 < r_1.
-}
-Prove: r != r_1.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
index 96fd464c7d661aba8da4e1b6b8c8939905c3d33e..70022706b9fbae3ba71f400040391c85dd2f61ae 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
@@ -9,13 +9,6 @@
------------------------------------------------------------
Goal Assertion (file unit_call.i, line 14):
-Assume {
- Type: is_sint32(r_1) /\ is_sint32(r).
- (* Call 'f' *)
- Have: r < 0.
- (* Call 'f' *)
- Have: 0 < r_1.
-}
-Prove: r != r_1.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
index b8222c6a9e63711f4596018b136d7399ad70a120..c334ef3718ad2f469e9931a12cf58eab280775db 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.0.res.oracle
@@ -12,8 +12,6 @@ Goal Assertion 'OUT' (file unit_cast.i, line 5):
unit_cast.i:4: warning from Typed Model:
- Warning: Hide sub-term definition
Reason: Cast with incompatible pointers types (source: sint32*) (target: sint8*)
-Let x = Mchar_0[w].
-Assume { Type: is_sint8(x). (* Heap *) Type: sconst(Mchar_0). }
-Prove: x <= 255.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
index 569fa012199a552edef54840ecb9189763856ed4..5d4f10b4737c1a8762185d5d66436e715bc2281d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_cast.1.res.oracle
@@ -12,8 +12,6 @@ Goal Assertion 'OUT' (file unit_cast.i, line 5):
unit_cast.i:4: warning from Typed Model:
- Warning: Hide sub-term definition
Reason: Cast with incompatible pointers types (source: sint32*) (target: sint8*)
-Let x = Mchar_0[w].
-Assume { Type: is_sint8(x). (* Heap *) Type: sconst(Mchar_0). }
-Prove: x <= 255.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
index ea0127e5c7dd06b90b62a784d82ab37136ae8a31..6f871cd6fc4d62ac24e925302c564e5ac6df812a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
@@ -16,7 +16,7 @@ Let x_1 = lsr(x, 31).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i <= 30) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 30).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 1))), lsl(1, 1 + i)) != 0) <->
(land(x, lsl(1, i)) != 0).
@@ -32,7 +32,7 @@ Let x_2 = lsr(x, 32 - n).
Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_2).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
@@ -65,7 +65,7 @@ Let x_2 = lsr(x, 64 - n).
Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_2).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
@@ -103,7 +103,7 @@ Let x_1 = lsr(x, 1).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i <= 30) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 30).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 31))), lsl(1, i)) != 0) <->
(land(x, lsl(1, 1 + i)) != 0).
@@ -119,7 +119,7 @@ Let x_2 = -n.
Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
@@ -152,7 +152,7 @@ Let x_2 = -n.
Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_1).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 4f262f161254f1b344217bfc2758b944c554031c..557801a559852a34dc42cbdb76461febdfc245a5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
@@ -51,24 +51,13 @@ Prove: x2_0 = v.
Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 57)
:
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 58)
:
-Let m = p[k <- v].
-Assume {
- Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
- IsArray_sint32(m) /\ is_sint32(1 + k).
- (* Pre-condition *)
- Have: (0 <= k) /\ (k <= 8).
- (* Call 'job' *)
- Have: (k <= 9) /\ EqArray_int(10, m, p[k <- x1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -140,24 +129,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 70)
:
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 71)
:
-Let m = q[k <- v].
-Assume {
- Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
- is_sint32(1 + k).
- (* Pre-condition *)
- Have: (0 <= k) /\ (k <= 8).
- (* Call 'job2' *)
- Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -229,24 +207,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 83)
:
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 84)
:
-Let m = q[k <- v].
-Assume {
- Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
- is_sint32(1 + k).
- (* Pre-condition *)
- Have: (0 <= k) /\ (k <= 8).
- (* Call 'job3' *)
- Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
index a96c98731e45f72d2106339b9b9ca016604b8ded..0cc485057a91f86a7a1e48c1024cfe329cae413e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_collect.1.res.oracle
@@ -51,24 +51,13 @@ Prove: x2_0 = v.
Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 57)
:
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition (file user_collect.i, line 15) in 'job'' in 'caller' at call 'job' (file user_collect.i, line 58)
:
-Let m = p[k <- v].
-Assume {
- Type: IsArray_sint32(p) /\ is_sint32(k) /\ is_sint32(x1_0) /\
- IsArray_sint32(m) /\ is_sint32(1 + k).
- (* Pre-condition *)
- Have: (0 <= k) /\ (k <= 8).
- (* Call 'job' *)
- Have: (k <= 9) /\ EqArray_int(10, m, p[k <- x1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -140,24 +129,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 70)
:
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition (file user_collect.i, line 26) in 'job2'' in 'caller2' at call 'job2' (file user_collect.i, line 71)
:
-Let m = q[k <- v].
-Assume {
- Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
- is_sint32(1 + k).
- (* Pre-condition *)
- Have: (0 <= k) /\ (k <= 8).
- (* Call 'job2' *)
- Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -229,24 +207,13 @@ Prove: EqArray_S1_S(10, m_1, m_2[k <- s2_0]).
Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 83)
:
-Assume { Type: is_sint32(k). (* Pre-condition *) Have: (0 <= k) /\ (k <= 8).
-}
-Prove: k <= 9.
+Prove: true.
------------------------------------------------------------
Goal Instance of 'Pre-condition (file user_collect.i, line 37) in 'job3'' in 'caller3' at call 'job3' (file user_collect.i, line 84)
:
-Let m = q[k <- v].
-Assume {
- Type: IsArray_S1_S(q) /\ IsS1_S(s1_0) /\ is_sint32(k) /\ IsArray_S1_S(m) /\
- is_sint32(1 + k).
- (* Pre-condition *)
- Have: (0 <= k) /\ (k <= 8).
- (* Call 'job3' *)
- Have: (k <= 9) /\ EqArray_S1_S(10, m, q[k <- s1_0]).
-}
-Prove: (-1) <= k.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 3941f8836e33495cea3f23d2e0b01ce118191efc..39e37a366cc59e64e9fe4893c56902f393af1c6e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -18,7 +18,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < n) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 < n).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
@@ -43,7 +43,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (i_1 <= i) /\ (0 <= i_1) /\ is_sint32(i_1).
+ When: (i_1 <= i) /\ (0 <= i_1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
@@ -68,24 +68,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file user_init.i, line 16):
-Let a_1 = shift_sint32(a, 0).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: (region(a.base) <= 0) /\ linked(Malloc_0).
- (* Pre-condition *)
- Have: valid_rw(Malloc_0, a_1, n).
- (* Invariant 'Range' *)
- Have: 0 <= n.
- (* Invariant 'Range' *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant 'Partial' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_1)] = v))).
- (* Then *)
- Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index df2b7d55d13f031670627d5d6f609d33a08926eb..418fe8936dd4043f4655d28fc42f1a71cdbe472b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -18,7 +18,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < n) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 < n).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
@@ -43,7 +43,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (i_1 <= i) /\ (0 <= i_1) /\ is_sint32(i_1).
+ When: (i_1 <= i) /\ (0 <= i_1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
@@ -68,24 +68,7 @@ Prove: true.
------------------------------------------------------------
Goal Preservation of Invariant 'Range' (file user_init.i, line 16):
-Let a_1 = shift_sint32(a, 0).
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Heap *)
- Type: (region(a.base) <= 0) /\ linked(Malloc_0).
- (* Pre-condition *)
- Have: valid_rw(Malloc_0, a_1, n).
- (* Invariant 'Range' *)
- Have: 0 <= n.
- (* Invariant 'Range' *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant 'Partial' *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_1)] = v))).
- (* Then *)
- Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
index 409348e3f43cc5f6baf5e91d530c0238a2f03c19..a0ad9eb6560ad6a0eb083c7c994e98c4fab964e8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
@@ -45,27 +45,12 @@ Prove: L_fact(n) = F1_0.
------------------------------------------------------------
Goal Preservation of Invariant (file user_rec.i, line 15):
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i) /\
- is_sint32(L_fact(i - 1)).
- (* Else *)
- Have: 2 <= n.
- (* Invariant *)
- Have: 0 < n.
- (* Invariant *)
- Have: L_fact(1) = 1.
- (* Invariant *)
- Have: (2 <= i) /\ (i <= (1 + n)).
- (* Then *)
- Have: i <= n.
-}
-Prove: 0 < i.
+Prove: true.
------------------------------------------------------------
Goal Establishment of Invariant (file user_rec.i, line 15):
-Assume { Type: is_sint32(n). (* Else *) Have: 2 <= n. }
-Prove: 0 < n.
+Prove: true.
------------------------------------------------------------
@@ -181,8 +166,7 @@ Prove: if (n <= 1) then (i = 1) else (0 < i).
------------------------------------------------------------
Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 28):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
------------------------------------------------------------
@@ -270,8 +254,7 @@ Prove: if (n <= 1) then (x_1 = n_1) else (n_1 <= x_1).
------------------------------------------------------------
Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 41):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
index 56da8ae60125b5030fabb2fcc1b26daaae7c89fb..f5f40e3f1169944a0c2c8409db455eed6d2d053b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
@@ -45,27 +45,12 @@ Prove: L_fact(n) = F1_0.
------------------------------------------------------------
Goal Preservation of Invariant (file user_rec.i, line 15):
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i) /\
- is_sint32(L_fact(i - 1)).
- (* Else *)
- Have: 2 <= n.
- (* Invariant *)
- Have: 0 < n.
- (* Invariant *)
- Have: L_fact(1) = 1.
- (* Invariant *)
- Have: (2 <= i) /\ (i <= (1 + n)).
- (* Then *)
- Have: i <= n.
-}
-Prove: 0 < i.
+Prove: true.
------------------------------------------------------------
Goal Establishment of Invariant (file user_rec.i, line 15):
-Assume { Type: is_sint32(n). (* Else *) Have: 2 <= n. }
-Prove: 0 < n.
+Prove: true.
------------------------------------------------------------
@@ -181,8 +166,7 @@ Prove: if (n <= 1) then (i = 1) else (0 < i).
------------------------------------------------------------
Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 28):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
------------------------------------------------------------
@@ -270,8 +254,7 @@ Prove: if (n <= 1) then (x_1 = n_1) else (n_1 <= x_1).
------------------------------------------------------------
Goal Establishment of Invariant 'RANGE' (file user_rec.i, line 41):
-Assume { Type: is_sint32(n). }
-Prove: (0 < n) \/ (n <= 1).
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
index db9cadfc9678a6f80d4af03f0636f8e3bfc4a625..764c77ab83c3656ea9e0dc9daa4c6cdc74f9add3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
@@ -5,11 +5,10 @@
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_job_assert : Valid
+[wp] [Qed] Goal typed_job_assert : Valid
[wp] Proved goals: 1 / 1
- Qed: 0
- Alt-Ergo: 1
+ Qed: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- job - 1 1 100%
+ job 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
index 8bfa5ac6000ca0903dd92d29100a3389678b89bc..a64f3428fb96e557ff0b662416073aeb092a44a1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle
@@ -5,11 +5,10 @@
[wp] unit_cast.i:4: Warning:
Cast with incompatible pointers types (source: sint32*) (target: sint8*)
[wp] 1 goal scheduled
-[wp] [Alt-Ergo] Goal typed_f_assert_OUT : Valid
+[wp] [Qed] Goal typed_f_assert_OUT : Valid
[wp] Proved goals: 1 / 1
- Qed: 0
- Alt-Ergo: 1
+ Qed: 1
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f - 1 1 100%
+ f 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
index 66c3467dac6402c11221309cd39da4377c2b1399..2b77015db8f380ff4d15f77143db07e7c94b81ac 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle
@@ -21,29 +21,29 @@
[wp] [Qed] Goal typed_caller_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller_ensures_P1 : Valid
[wp] [Alt-Ergo] Goal typed_caller_ensures_P2 : Valid
-[wp] [Alt-Ergo] Goal typed_caller_call_job_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller_call_job_2_requires : Valid
+[wp] [Qed] Goal typed_caller_call_job_requires : Valid
+[wp] [Qed] Goal typed_caller_call_job_2_requires : Valid
[wp] [Qed] Goal typed_caller2_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller2_ensures_R : Valid
-[wp] [Alt-Ergo] Goal typed_caller2_call_job2_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller2_call_job2_2_requires : Valid
+[wp] [Qed] Goal typed_caller2_call_job2_requires : Valid
+[wp] [Qed] Goal typed_caller2_call_job2_2_requires : Valid
[wp] [Qed] Goal typed_caller3_ensures_K : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q1 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_Q2 : Valid
[wp] [Alt-Ergo] Goal typed_caller3_ensures_R : Valid
-[wp] [Alt-Ergo] Goal typed_caller3_call_job3_requires : Valid
-[wp] [Alt-Ergo] Goal typed_caller3_call_job3_2_requires : Valid
+[wp] [Qed] Goal typed_caller3_call_job3_requires : Valid
+[wp] [Qed] Goal typed_caller3_call_job3_2_requires : Valid
[wp] Proved goals: 32 / 32
- Qed: 17
- Alt-Ergo: 15
+ Qed: 23
+ Alt-Ergo: 9
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
job 5 - 5 100%
job2 5 - 5 100%
job3 4 1 5 100%
- caller 1 4 5 100%
- caller2 1 5 6 100%
- caller3 1 5 6 100%
+ caller 3 2 5 100%
+ caller2 3 3 6 100%
+ caller3 3 3 6 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
index 6ac1e79c7df3e5bf433947a28cf46fea7691b115..03608893948267aa0621d6f529a4c5f445a8509a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle
@@ -11,7 +11,7 @@
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Partial_established : Valid
-[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_init_loop_invariant_Range_preserved : Valid
[wp] [Qed] Goal typed_init_loop_invariant_Range_established : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part1 : Valid
[wp] [Qed] Goal typed_init_loop_assigns_part2 : Valid
@@ -101,11 +101,11 @@
[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_call_init_requires_2 : Valid
[wp] Proved goals: 97 / 97
- Qed: 52
- Alt-Ergo: 40
+ Qed: 53
+ Alt-Ergo: 39
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- init 7 4 11 100%
+ init 8 3 11 100%
init_t1 6 4 10 100%
init_t2_v1 9 8 17 100%
init_t2_v2 9 8 17 100%
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
index 303439c8d14682fb72b73fae8a4454377c6728da..e5acf75e0c54333f32b8eb415037cb422f1bf4b1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle
@@ -4,8 +4,8 @@
[wp] Warning: Missing RTE guards
[wp] 18 goals scheduled
[wp] [Alt-Ergo] Goal typed_F1_ensures : Valid
-[wp] [Alt-Ergo] Goal typed_F1_loop_invariant_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_F1_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_F1_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_F1_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_F1_loop_invariant_2_preserved : Valid
[wp] [Alt-Ergo] Goal typed_F1_loop_invariant_2_established : Valid
[wp] [Qed] Goal typed_F1_loop_assigns : Valid
@@ -13,20 +13,20 @@
[wp] [Alt-Ergo] Goal typed_F2_loop_invariant_PART_preserved : Valid
[wp] [Alt-Ergo] Goal typed_F2_loop_invariant_PART_established : Valid
[wp] [Alt-Ergo] Goal typed_F2_loop_invariant_RANGE_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_F2_loop_invariant_RANGE_established : Valid
+[wp] [Qed] Goal typed_F2_loop_invariant_RANGE_established : Valid
[wp] [Qed] Goal typed_F2_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_F4_ensures : Valid
[wp] [Alt-Ergo] Goal typed_F4_loop_invariant_NEVER_preserved : Valid
[wp] [Alt-Ergo] Goal typed_F4_loop_invariant_NEVER_established : Valid
[wp] [Alt-Ergo] Goal typed_F4_loop_invariant_RANGE_preserved : Valid
-[wp] [Alt-Ergo] Goal typed_F4_loop_invariant_RANGE_established : Valid
+[wp] [Qed] Goal typed_F4_loop_invariant_RANGE_established : Valid
[wp] [Qed] Goal typed_F4_loop_assigns : Valid
[wp] Proved goals: 18 / 18
- Qed: 3
- Alt-Ergo: 15
+ Qed: 7
+ Alt-Ergo: 11
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- F1 1 5 6 100%
- F2 1 5 6 100%
- F4 1 5 6 100%
+ F1 3 3 6 100%
+ F2 2 4 6 100%
+ F4 2 4 6 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index 2389a4fcd586f975c134e67c237dafd499d11824..fbc663bb95acbeac2fcb60827b93d357b57d006a 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
@@ -41,24 +41,7 @@ Prove: Mint_0[shift_sint32(a, i)] = v[i].
------------------------------------------------------------
Goal Preservation of Invariant (file caveat2.i, line 21):
-Assume {
- Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
- (* Pre-condition *)
- Have: n <= 3.
- Have: ({ Init_p_0 with Init_F1_S_n = true }) = Init_p_0.
- (* Invariant *)
- Have: 0 <= n.
- (* Loop assigns ... *)
- Have: ({ Init_p_0 with Init_F1_S_a = v }) = Init_p_0.
- (* Invariant *)
- Have: (0 <= i) /\ (i <= n).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (Mint_0[shift_sint32(global(G_b_26), i_1)] = v_1[i_1]))).
- (* Then *)
- Have: i < n.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
index 82c8bbe685e4f64775f367b669c89d585e07a23c..8411b76b58db2c71fdfa5e787b3a7c09794680cf 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat_range.res.oracle
@@ -51,22 +51,7 @@ Prove: a_1[shiftfield_F1_S_g(shift_S1_S(a, i))] = 2.
------------------------------------------------------------
Goal Preservation of Invariant (file caveat_range.i, line 19):
-Let a = global(G_p_22).
-Let a_1 = havoc(Mint_undef_0, Mint_0, shift_S1_S(a, 0), 20).
-Assume {
- Type: is_sint32(i) /\ is_sint32(1 + i).
- (* Invariant *)
- Have: (0 <= i) /\ (i <= 10).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_1[shiftfield_F1_S_f(shift_S1_S(a, i_1))] = 1))).
- (* Invariant *)
- Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
- (a_1[shiftfield_F1_S_g(shift_S1_S(a, i_1))] = 2))).
- (* Then *)
- Have: i <= 9.
-}
-Prove: (-1) <= i.
+Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
index 47170bfb5f1ba9b6be9395dfe482e1cbe04ef482..1797f0fdbbb7a1c740799dd113168dba2f61f0e3 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle
@@ -6,7 +6,7 @@
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_caveat_job_ensures_N : Valid
[wp] [Alt-Ergo] Goal typed_caveat_job_ensures_A : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_job_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_caveat_job_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_caveat_job_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_caveat_job_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_caveat_job_loop_invariant_2_established : Valid
@@ -14,11 +14,11 @@
[wp] [Qed] Goal typed_caveat_job_assigns_part1 : Valid
[wp] [Qed] Goal typed_caveat_job_assigns_part2 : Valid
[wp] Proved goals: 9 / 9
- Qed: 6
- Alt-Ergo: 3
+ Qed: 7
+ Alt-Ergo: 2
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- job 6 3 9 100%
+ job 7 2 9 100%
------------------------------------------------------------
[wp] caveat2.i:17: Warning:
Memory model hypotheses for function 'job':
diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
index 308353df0fe312ab678317f2893c12542649462d..4dd118b0742599e74b2c21bcfc012590ee771f5f 100644
--- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle
@@ -5,7 +5,7 @@
[wp] 12 goals scheduled
[wp] [Alt-Ergo] Goal typed_caveat_reset_ensures : Valid
[wp] [Alt-Ergo] Goal typed_caveat_reset_ensures_2 : Valid
-[wp] [Alt-Ergo] Goal typed_caveat_reset_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_caveat_reset_loop_invariant_preserved : Valid
[wp] [Qed] Goal typed_caveat_reset_loop_invariant_established : Valid
[wp] [Alt-Ergo] Goal typed_caveat_reset_loop_invariant_2_preserved : Valid
[wp] [Qed] Goal typed_caveat_reset_loop_invariant_2_established : Valid
@@ -16,11 +16,11 @@
[wp] [Qed] Goal typed_caveat_reset_loop_assigns_part3 : Valid
[wp] [Qed] Goal typed_caveat_reset_assigns : Valid
[wp] Proved goals: 12 / 12
- Qed: 7
- Alt-Ergo: 5
+ Qed: 8
+ Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- reset 7 5 12 100%
+ reset 8 4 12 100%
------------------------------------------------------------
[wp] caveat_range.i:16: Warning:
Memory model hypotheses for function 'reset':