From 3f20b13537befe011e6035621bd70e943879c58d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 21 Jan 2021 10:21:28 +0100
Subject: [PATCH] [WP] fixes smp_eq_with_lor (adds an integrity test)
---
src/plugins/wp/tests/wp_acsl/issue_A228.c | 34 +++++++++++++++++++
.../wp_acsl/oracle/issue_A228.res.oracle | 11 ++++++
.../oracle_qualif/issue_A228.res.oracle | 11 ++++++
3 files changed, 56 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/issue_A228.c
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/issue_A228.c b/src/plugins/wp/tests/wp_acsl/issue_A228.c
new file mode 100644
index 00000000000..42d685b222f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/issue_A228.c
@@ -0,0 +1,34 @@
+Bool A, B;
+
+/*@
+ ensures GOAL: \result ≡ 255;
+ */
+unsigned job(void)
+{
+ _Bool a0;
+ _Bool a1;
+ _Bool a2;
+ _Bool a3;
+ _Bool a4;
+ _Bool a5;
+ _Bool a6;
+ _Bool a7;
+ a0 = 1;
+ a1 = 1;
+ a2 = 1;
+ a4 = 1;
+ a3 = 1;
+ a5 = 1;
+ a6 = A;
+ a7 = B;
+ //*integrity_tests =
+ return
+ ((unsigned int)a0 << 0) |
+ ((unsigned int)a1 << 1) |
+ ((unsigned int)a2 << 2) |
+ ((unsigned int)a3 << 3) |
+ ((unsigned int)a4 << 4) |
+ ((unsigned int)a5 << 5) |
+ ((unsigned int)a6 << 6) |
+ ((unsigned int)a7 << 7);
+}
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
new file mode 100644
index 00000000000..e1e22036ebe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/issue_A228.res.oracle
@@ -0,0 +1,11 @@
+# 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.
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle
new file mode 100644
index 00000000000..e1e22036ebe
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle
@@ -0,0 +1,11 @@
+# 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.
--
GitLab