From 62fb6a2f318f9ed624a32f78736e61f95dd02b68 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Feb 2021 14:55:21 +0100
Subject: [PATCH] [wp] renaming & ordering & prop selection

test cases 1 & 2 has prop selection
---
 .../wp_typed/oracle/user_init.0.res.oracle    | 24 ++++++++++++-------
 .../wp_typed/oracle/user_init.1.res.oracle    | 24 ++++++++++++-------
 .../oracle_qualif/user_init.0.res.oracle      |  2 +-
 .../oracle_qualif/user_init.1.res.oracle      |  7 +-----
 .../oracle_qualif/user_init.2.res.oracle      |  7 +-----
 5 files changed, 35 insertions(+), 29 deletions(-)

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 e1453e78f00..e73a0f10013 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 52e4c648900..81badf95a29 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 890545f1a90..fa0b0883eae 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 71a1c37ecc6..d063e017221 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 73b6604f313..612a2377cfd 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)
 ------------------------------------------------------------
-- 
GitLab