From f8aa09e2db793fc69d459e7b44a48d63db99c168 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Feb 2021 12:13:48 +0100
Subject: [PATCH] [wp] naming pre-conditions
---
.../oracle/generalized_checks.res.oracle | 22 ++++++++++++++-----
1 file changed, 16 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
index d3f8259be9d..cb8dc37d91b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -36,7 +36,9 @@ Goal Post-condition 'R1,ko' in 'caller':
Assume {
Type: is_sint32(caller_0) /\ is_sint32(x).
(* Pre-condition *)
- Have: P_A(x) /\ P_CA1(x).
+ Have: P_A(x).
+ (* Pre-condition *)
+ Have: P_CA1(x).
(* Call 'job' *)
Have: P_B(caller_0).
}
@@ -48,7 +50,9 @@ Goal Post-condition 'R2,ko' in 'caller':
Assume {
Type: is_sint32(caller_0) /\ is_sint32(x).
(* Pre-condition *)
- Have: P_A(x) /\ P_CA1(x).
+ Have: P_A(x).
+ (* Pre-condition *)
+ Have: P_CA1(x).
(* Call 'job' *)
Have: P_B(caller_0).
}
@@ -86,7 +90,13 @@ Prove: true.
Goal Instance of 'Pre-condition 'CA2,ko' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
:
-Assume { Type: is_sint32(x). (* Pre-condition *) Have: P_A(x) /\ P_CA1(x). }
+Assume {
+ Type: is_sint32(x).
+ (* Pre-condition *)
+ Have: P_A(x).
+ (* Pre-condition *)
+ Have: P_CA1(x).
+}
Prove: P_CA2(x).
------------------------------------------------------------
@@ -98,7 +108,7 @@ Goal Post-condition 'B' in 'job':
Let x_1 = L_F(x).
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
- (* Pre-condition *)
+ (* Pre-condition 'A' *)
Have: P_A(x).
}
Prove: P_B(x_1).
@@ -109,7 +119,7 @@ Goal Post-condition 'CB1' in 'job':
Let x_1 = L_F(x).
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
- (* Pre-condition *)
+ (* Pre-condition 'A' *)
Have: P_A(x).
}
Prove: P_CB1(x_1).
@@ -120,7 +130,7 @@ Goal Post-condition 'CB2,ko' in 'job':
Let x_1 = L_F(x).
Assume {
Type: is_sint32(x) /\ is_sint32(x_1).
- (* Pre-condition *)
+ (* Pre-condition 'A' *)
Have: P_A(x).
}
Prove: P_CB2(x_1).
--
GitLab