From 9dce6844b5b71bec793cd415039a3f7ccca234af Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 2 Feb 2022 14:48:59 +0100
Subject: [PATCH] [Wp] updated oracles of the default tests
---
.../tests/wp/oracle/wp_call_pre.2.res.oracle | 9 +-
.../tests/wp/oracle/wp_call_pre.3.res.oracle | 9 +-
.../wp/tests/wp_acsl/oracle/arith.res.oracle | 6 +-
.../wp_acsl/oracle/assigns_path.res.oracle | 18 +-
.../wp_acsl/oracle/assigns_range.res.oracle | 24 +--
.../wp_acsl/oracle/chunk_typing.res.oracle | 192 +-----------------
.../wp_acsl/oracle/looplabels.res.oracle | 25 +--
.../wp_acsl/oracle/postassigns.res.oracle | 11 +-
.../wp_acsl/oracle/simpl_is_type.res.oracle | 43 +---
.../terminates_variant_option.1.res.oracle | 13 +-
.../wp/tests/wp_bts/oracle/bts779.res.oracle | 4 +-
.../tests/wp_bts/oracle/issue_751.res.oracle | 13 +-
.../wp_plugin/oracle/combined.res.oracle | 19 +-
.../wp/tests/wp_plugin/oracle/copy.res.oracle | 27 +--
.../tests/wp_plugin/oracle/prenex.res.oracle | 58 +-----
.../tests/wp_plugin/oracle/repeat.res.oracle | 46 +----
.../wp_plugin/oracle/sequence.res.oracle | 48 +----
.../wp_plugin/oracle/string_c.res.oracle | 80 +-------
.../tests/wp_tip/oracle/modmask.0.res.oracle | 22 +-
.../script/check_lemma_and_modulo_u.json | 4 +-
.../script/check_lemma_and_modulo_us_255.json | 3 +-
.../tests/wp_tip/oracle/modmask.1.res.oracle | 22 +-
.../script/check_lemma_and_modulo_u.json | 4 +-
.../script/check_lemma_and_modulo_us_255.json | 3 +-
.../wp_typed/oracle/unit_call.0.res.oracle | 9 +-
.../wp_typed/oracle/unit_call.1.res.oracle | 9 +-
.../wp_typed/oracle/unit_cast.0.res.oracle | 4 +-
.../wp_typed/oracle/unit_cast.1.res.oracle | 4 +-
.../wp_typed/oracle/user_collect.0.res.oracle | 45 +---
.../wp_typed/oracle/user_collect.1.res.oracle | 45 +---
.../wp_typed/oracle/user_init.0.res.oracle | 19 +-
.../wp_typed/oracle/user_init.1.res.oracle | 19 +-
.../wp_typed/oracle/user_rec.0.res.oracle | 25 +--
.../wp_typed/oracle/user_rec.1.res.oracle | 25 +--
.../tests/wp_usage/oracle/caveat2.res.oracle | 19 +-
.../wp_usage/oracle/caveat_range.res.oracle | 17 +-
36 files changed, 71 insertions(+), 872 deletions(-)
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 4f4bf9be94a..8ee9e5fdf9b 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 15d814ca6a8..63c5f1576f9 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_acsl/oracle/arith.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/arith.res.oracle
index 9e0b53a7ea0..745239a656b 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 b8e9db163f8..aaf2d71df37 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 f06695c9f12..cb23d6906cf 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/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 4c3b2575f9e..18d052e09ff 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 b97ad879047..bb59f39de14 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 45bac9e9756..68a4d2e6a12 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 e3393701a39..80262cbe5dc 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
@@ -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.
------------------------------------------------------------
@@ -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.
------------------------------------------------------------
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 37df7d0a04a..dc049f029f8 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_bts/oracle/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts779.res.oracle
index 5683dde8aeb..214d5ef2e3c 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 18231f2787c..2e738afb004 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_plugin/oracle/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/combined.res.oracle
index 977dad88e4b..ff49553d883 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 45e2914bd43..5e9cbd10437 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/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/prenex.res.oracle
index 2721d73c750..ed64f075c63 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 99192ce42a7..72cc29ecc9f 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 fedcdb66fb6..156a43c16d4 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 c1383873535..faadd1df808 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_tip/oracle/modmask.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/modmask.0.res.oracle
index dd1cd3edf7d..b65abf98b7f 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 e40e8863e3c..84b0af02539 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 0232433c576..67fe782ea8a 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 dd1cd3edf7d..b65abf98b7f 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 7d2e4b041e8..51fbe949924 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 a56490bac7a..c16388ade5d 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_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
index 7088dae230b..81b6a3c63ea 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 96fd464c7d6..70022706b9f 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 b8222c6a9e6..c334ef3718a 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 569fa012199..5d4f10b4737 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_collect.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_collect.0.res.oracle
index 4f262f16125..557801a5598 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 a96c98731e4..0cc485057a9 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 85d53722544..39e37a366cc 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
@@ -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 2abe7e2f668..418fe8936dd 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
@@ -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 409348e3f43..a0ad9eb6560 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 56da8ae6012..f5f40e3f116 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_usage/oracle/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat2.res.oracle
index 2389a4fcd58..fbc663bb95a 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 82c8bbe685e..8411b76b58d 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.
------------------------------------------------------------
--
GitLab