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 e1453e78f00b00eedd5171411a24d476a3abdac4..e73a0f100136a788210f0f92688f6d7036d9ec5b 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
@@ -2,11 +2,11 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal init_exits : Valid (Unreachable)
+[wp] Warning: Missing RTE guards
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function init
------------------------------------------------------------
@@ -20,7 +20,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 < n) /\ is_sint32(i_1).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= n.
(* Invariant 'Partial' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_2)] = v))).
@@ -43,7 +45,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= n.
(* Invariant 'Partial' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(a, i_2)] = v))).
@@ -68,7 +72,9 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= 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))).
@@ -108,7 +114,9 @@ Assume {
(* Goal *)
When: !invalid(Malloc_0, a_2, 1).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= 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))).
@@ -835,10 +843,10 @@ Assume {
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
((i_3 <= 19) ->
(((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (t2_2[i_4][i_3] = t2_0[i_4][i_3])))))).
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_0[i_4][i_3]))))).
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
}
@@ -1331,7 +1339,7 @@ Assume {
Have: i <= 9.
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = t2_0[i_4][i_3]))))).
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
}
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 52e4c648900f469687bc6129f102187cbef53360..81badf95a29a8e16c113baa7ff30109199227ff9 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
@@ -2,11 +2,11 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal init_exits : Valid (Unreachable)
+[wp] Warning: Missing RTE guards
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function init
------------------------------------------------------------
@@ -20,7 +20,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 < n) /\ is_sint32(i_1).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= n.
(* Invariant 'Partial' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(havoc(Mint_undef_0, Mint_0, a_1, n)[shift_sint32(a, i_2)] = v))).
@@ -43,7 +45,9 @@ Assume {
(* Goal *)
When: (0 <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= n.
(* Invariant 'Partial' *)
Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
(a_2[shift_sint32(a, i_2)] = v))).
@@ -68,7 +72,9 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= 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))).
@@ -108,7 +114,9 @@ Assume {
(* Goal *)
When: !invalid(Malloc_0, a_2, 1).
(* Pre-condition *)
- Have: (0 <= n) /\ valid_rw(Malloc_0, a_1, n).
+ Have: valid_rw(Malloc_0, a_1, n).
+ (* Pre-condition *)
+ Have: 0 <= 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))).
@@ -835,10 +843,10 @@ Assume {
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((0 <= i_3) -> ((i_4 <= 9) ->
((i_3 <= 19) ->
(((i_4 < 0) \/ (i_3 < 0) \/ (10 <= i_4) \/ (20 <= i_3)) ->
- (t2_0[i_4][i_3] = t2_2[i_4][i_3])))))).
+ (t2_2[i_4][i_3] = t2_0[i_4][i_3])))))).
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_2[i_4][i_3]))))).
+ ((i_3 <= 19) -> (t2_2[i_4][i_3] = t2_0[i_4][i_3]))))).
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
}
@@ -1331,7 +1339,7 @@ Assume {
Have: i <= 9.
(* Invariant 'Previous_i' *)
Have: forall i_4,i_3 : Z. ((0 <= i_4) -> ((i_4 < i) -> ((0 <= i_3) ->
- ((i_3 <= 19) -> (t2_0[i_4][i_3] = t2_1[i_4][i_3]))))).
+ ((i_3 <= 19) -> (t2_1[i_4][i_3] = t2_0[i_4][i_3]))))).
(* Invariant 'Partial_j' *)
Have: forall i_3 : Z. ((0 <= i_3) -> ((i_3 <= 19) -> (m[i_3] = v))).
}
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 890545f1a901bbb0eaec681155b688d75658e609..fa0b0883eae31e9e50dc79db27fb1cec785fdaca 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
@@ -2,11 +2,11 @@
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] [CFG] Goal init_exits : Valid (Unreachable)
+[wp] Warning: Missing RTE guards
[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
-[wp] Warning: Missing RTE guards
[wp] 92 goals scheduled
[wp] [Alt-Ergo] Goal typed_init_ensures : Valid
[wp] [Alt-Ergo] Goal typed_init_loop_invariant_Partial_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
index 71a1c37ecc6fac5af4a88d1151b8798d141a3ca8..d063e01722192b7cf2eb264e6ccc6a50b5e85dc3 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
@@ -1,11 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
-[wp] [CFG] Goal init_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Qed] Goal typed_init_t2_v2_loop_assigns_part1 : Valid
@@ -31,7 +26,7 @@
[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_init_t2_bis_v2_assigns_normal_part1 : Valid
[wp] [Script] Goal typed_init_t2_bis_v2_assigns_normal_part2 : Valid
-[wp] Proved goals: 28 / 28
+[wp] Proved goals: 23 / 23
Qed: 11
Script: 12
Alt-Ergo: 0 (unsuccess: 12)
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
index 73b6604f313f1b3c18ba90b8824a3f4c14e24982..612a2377cfd3ce0ff68a451c5abbf4fc60a18c1c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.2.res.oracle
@@ -1,11 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_typed/user_init.i (no preprocessing)
[wp] Running WP plugin...
-[wp] [CFG] Goal init_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_v1_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_v2_exits : Valid (Unreachable)
-[wp] [CFG] Goal init_t2_v3_exits : Valid (Unreachable)
[wp] Warning: Missing RTE guards
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_init_t2_v1_loop_assigns_part1 : Valid
@@ -24,7 +19,7 @@
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_exit_part3 : Valid
[wp] [Qed] Goal typed_init_t2_bis_v1_assigns_normal_part1 : Valid
[wp] [Alt-Ergo] Goal typed_init_t2_bis_v1_assigns_normal_part2 : Unsuccess
-[wp] Proved goals: 12 / 21
+[wp] Proved goals: 7 / 16
Qed: 7
Alt-Ergo: 0 (unsuccess: 9)
------------------------------------------------------------