From 3109c12f8d37c4c1087658ef8bc24b11b762794b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Feb 2021 15:22:21 +0100
Subject: [PATCH] [wp] naming pre-conditions
---
.../tests/wp_hoare/oracle/logicarr.res.oracle | 18 +++++++++++++++---
1 file changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
index 921a9d48bb6..690c5552852 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/logicarr.res.oracle
@@ -17,7 +17,11 @@ Assume {
IsArray_sint32(Array_sint32(a, 10, Mint_0)) /\ is_sint32(x) /\
IsArray_sint32(Array_sint32(a, 10, m)).
(* Pre-condition *)
- Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
+ Have: (0 <= i) /\ (i <= 9).
+ (* Pre-condition *)
+ Have: (0 <= j) /\ (j <= 9).
+ (* Pre-condition *)
+ Have: (0 <= k) /\ (k <= 9).
}
Prove: P_p_pointer(m, Mint_0, shift_sint32(a, 0), i, j).
@@ -35,7 +39,11 @@ Assume {
Type: is_sint32(i) /\ is_sint32(j) /\ is_sint32(k) /\ IsArray_sint32(m) /\
is_sint32(x) /\ IsArray_sint32(m_1).
(* Pre-condition *)
- Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
+ Have: (0 <= i) /\ (i <= 9).
+ (* Pre-condition *)
+ Have: (0 <= j) /\ (j <= 9).
+ (* Pre-condition *)
+ Have: (0 <= k) /\ (k <= 9).
}
Prove: P_p_arrays(m, i, m_1, j).
@@ -53,7 +61,11 @@ Assume {
IsArray_sint32(Array_sint32(a, 10, Mint_0)) /\ is_sint32(x) /\
IsArray_sint32(m).
(* Pre-condition *)
- Have: (0 <= i) /\ (0 <= j) /\ (0 <= k) /\ (i <= 9) /\ (j <= 9) /\ (k <= 9).
+ Have: (0 <= i) /\ (i <= 9).
+ (* Pre-condition *)
+ Have: (0 <= j) /\ (j <= 9).
+ (* Pre-condition *)
+ Have: (0 <= k) /\ (k <= 9).
}
Prove: P_p_dummy(m, j, k).
--
GitLab