From 754e522ceb12b5e498f299566dd7208804b93d34 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 29 Jan 2021 10:01:45 +0100
Subject: [PATCH] [WP] fixes a typo in a test.
---
src/plugins/wp/tests/wp_acsl/issue_A228.c | 2 +-
.../wp_acsl/oracle/issue_A228.res.oracle | 20 ++++++++++---------
2 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/issue_A228.c b/src/plugins/wp/tests/wp_acsl/issue_A228.c
index 42d685b222f..6d970cf28e1 100644
--- a/src/plugins/wp/tests/wp_acsl/issue_A228.c
+++ b/src/plugins/wp/tests/wp_acsl/issue_A228.c
@@ -1,4 +1,4 @@
-Bool A, B;
+_Bool A, B;
/*@
ensures GOAL: \result ≡ 255;
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle
index e1e22036ebe..e06b9fc16c1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle
@@ -1,11 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/issue_A228.c (with preprocessing)
-[kernel] :0:
- syntax error:
- Location: between <unknown> and 1:5, before or at token: A
-
- 1 Bool A, B;
-
- 2
- 3 /*@
-[kernel] Frama-C aborted: invalid user input.
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition 'GOAL' in 'job':
+Assume { Type: is_bool(A) /\ is_bool(B). }
+Prove: land(-64, lor(to_uint32(lsl(A, 6)), to_uint32(lsl(B, 7)))) = 192.
+
+------------------------------------------------------------
--
GitLab