From af8b4e103c6154d5cc6fb92efa352dcedbb362f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 15 Feb 2021 17:39:33 +0100
Subject: [PATCH] [wp] pre-conditions naming
---
src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle | 2 +-
src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle
index 3e326765311..22064c851cd 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle
@@ -165,7 +165,7 @@ Assume {
is_sint32(x_4) /\ is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7).
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(r.base) <= 0).
- (* Pre-condition *)
+ (* Pre-condition 'KO' *)
Have: P_OBS(x, x_1, x_2).
}
Prove: P_OBS(x_5, x_6, x_7).
diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
index 7f6f4e13162..2801d3fd0e5 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle
@@ -62,7 +62,7 @@ Let x_4 = x + x_1.
Assume {
Type: is_sint32(r) /\ is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
is_sint32(x_3) /\ is_sint32(x_4).
- (* Pre-condition *)
+ (* Pre-condition 'KO' *)
Have: P_OBS(x, x_1, r).
}
Prove: P_OBS(x_2, x_3, x_4).
--
GitLab