From 1d056b0880ba96b956715d28fa48945ca0a22c6f Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 1 Feb 2022 17:19:05 +0100
Subject: [PATCH] [WP] oracle updated
---
.../wp/tests/wp/oracle/wp_behav.res.oracle | 2 +-
.../wp/tests/wp_acsl/oracle/axioms.res.oracle | 2 +-
.../wp_acsl/oracle/simpl_is_type.res.oracle | 10 +++----
.../wp_acsl/oracle/unit_bit_test.res.oracle | 2 +-
...tion_loop_invariant_inv1_ok_preserved.json | 30 +++++++++----------
.../tests/wp_plugin/oracle/cint.3.res.oracle | 3 +-
.../wp/tests/wp_plugin/oracle/loop.res.oracle | 4 +--
.../script/lemma_res_n.json | 2 +-
.../script/lemma_res_y.json | 2 +-
.../script/unrolled_loop_ensures_zero.json | 2 +-
.../script/lemma_ByInd.json | 6 ++--
.../script/lemma_j_incr_char.json | 2 +-
.../script/lemma_j_incr_short.json | 2 +-
.../unroll.0.session/script/lemma_LEFT.json | 3 +-
.../unroll.0.session/script/lemma_RIGHT.json | 3 +-
.../unroll.0.session/script/lemma_SUM.json | 3 +-
.../wp_typed/oracle/cast_fits.0.res.oracle | 2 +-
.../wp_typed/oracle/cast_fits.1.res.oracle | 2 +-
.../wp_typed/oracle/shift_lemma.0.res.oracle | 2 +-
.../wp_typed/oracle/shift_lemma.1.res.oracle | 2 +-
.../wp_typed/oracle/user_bitwise.0.res.oracle | 12 ++++----
.../wp_typed/oracle/user_init.0.res.oracle | 4 +--
.../wp_typed/oracle/user_init.1.res.oracle | 4 +--
23 files changed, 51 insertions(+), 55 deletions(-)
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 06a4d869938..7b055f9626f 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_acsl/oracle/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
index 17f0f3c5cb5..6a44c5e64ba 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/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index b96c22a4802..e3393701a39 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 *)
@@ -269,7 +269,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 +308,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 +340,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))).
@@ -457,7 +457,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/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
index cd6729ea2d5..f444ed8fb1b 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_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 2bbbd17af44..a9679b500c9 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_plugin/oracle/cint.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
index 13ce327181d..8204ab6fa78 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/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
index b346927e4d3..b35e3645528 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_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 c1f541d00af..ce1db3baf84 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 95cf3e5f295..6efc632858b 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/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 1c97c0efd6f..fee182f4fb2 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_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 2a359dbab3a..77a4f51c832 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 9ca995ee623..255539ba9f3 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 b07a8979875..97c383396b0 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 885feb947bd..cadd5e50101 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 75e4064cdb6..2c6b678d138 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 65a87aa59ca..60f8f7acd6c 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 207e9befdb7..91d993407e9 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 f456415436e..76f3b9532f3 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 3161feeff64..652ab955538 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 67d2f08869b..62c3c4fdabf 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/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
index ea0127e5c7d..6f871cd6fc4 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_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 3941f8836e3..85d53722544 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' *)
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 df2b7d55d13..2abe7e2f668 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' *)
--
GitLab