From 51e297816d84a197057111d69cb0e7189cf65b3f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 19 Dec 2019 11:22:11 +0100
Subject: [PATCH] [WP] add test to check goal for #775 is correctly generated
by Why3 API
---
src/plugins/wp/tests/wp_acsl/boolean.i | 16 ++++++
.../tests/wp_acsl/oracle/boolean.res.oracle | 50 +++++++++++++++++++
2 files changed, 66 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/boolean.i
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/boolean.i b/src/plugins/wp/tests/wp_acsl/boolean.i
new file mode 100644
index 00000000000..212b2117f66
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/boolean.i
@@ -0,0 +1,16 @@
+/* run.config
+OPT: -wp-prover alt-ergo -wp-gen
+*/
+ /*@
+ logic boolean u8_continue_f(unsigned char b) =
+ 0x80<=b && 0xC0 > b;
+ */
+
+ /*@
+ assigns \nothing;
+ ensures u8_continue_f(b) == \result==1;
+ */
+ int u8_is_continue(const unsigned char b)
+ {
+ return b >= 0x80 && b <= 0xBF;
+ }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
new file mode 100644
index 00000000000..0ae8f9eabef
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
@@ -0,0 +1,50 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
+[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
+[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
+[wp] 4 goals generated
+------------------------------------------------------------
+ Function u8_is_continue
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/boolean.i, line 11) in 'u8_is_continue':
+Assume {
+ Type: is_uint8(b) /\ is_sint32(u8_is_continue_0).
+ If 128 <= b
+ Then {
+ If b <= 191
+ Then { Have: u8_is_continue_0 = 1. }
+ Else { Have: u8_is_continue_0 = 0. }
+ }
+ Else { Have: u8_is_continue_0 = 0. }
+}
+Prove: (u8_is_continue_0 = 1) /\
+ ((L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0)).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'u8_is_continue' (1/3):
+Effect at line 15
+Prove: true.
+Prover Qed returns Valid
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'u8_is_continue' (2/3):
+Effect at line 15
+Prove: true.
+Prover Qed returns Valid
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'u8_is_continue' (3/3):
+Effect at line 15
+Prove: true.
+Prover Qed returns Valid
+
+------------------------------------------------------------
--
GitLab