From 071a7a1ebc53f3e59bc119b295db2237636634c1 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 7 Jan 2022 11:25:12 +0100
Subject: [PATCH] [WP] add a test of the introduced rule
---
src/plugins/wp/tests/wp_acsl/bitwise.i | 6 ++++++
src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle | 8 ++++++++
.../wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle | 8 +++++---
3 files changed, 19 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/bitwise.i b/src/plugins/wp/tests/wp_acsl/bitwise.i
index d9dcf8fe503..b2e5594f270 100644
--- a/src/plugins/wp/tests/wp_acsl/bitwise.i
+++ b/src/plugins/wp/tests/wp_acsl/bitwise.i
@@ -124,3 +124,9 @@ void lemma(unsigned a, unsigned b, unsigned k) {
//@ check ( a & b & 77 & ((1 << (k & 55))-1) ) == ( (a & b & 77) % (1 << (k & 55)) );
}
+
+//@ ensures \result == (x & 0xFF) ;
+unsigned char cast_uchar(int x) {
+ unsigned char c = x;
+ return c;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 351c09e561f..232b2653404 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -218,6 +218,14 @@ Assume {
}
Prove: b != a.
+------------------------------------------------------------
+------------------------------------------------------------
+ Function cast_uchar
+------------------------------------------------------------
+
+Goal Post-condition (file bitwise.i, line 128) in 'cast_uchar':
+Prove: true.
+
------------------------------------------------------------
------------------------------------------------------------
Function lemma
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index 946e96312f8..413c2326caa 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing bitwise.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 37 goals scheduled
+[wp] 38 goals scheduled
[wp] [Qed] Goal typed_band_ensures : Valid
[wp] [Qed] Goal typed_band_ensures_band0 : Valid
[wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
@@ -40,8 +40,9 @@
[wp] [Qed] Goal typed_lemma_check_5 : Valid
[wp] [Qed] Goal typed_lemma_check_6 : Valid
[wp] [Qed] Goal typed_lemma_check_7 : Valid
-[wp] Proved goals: 37 / 37
- Qed: 33
+[wp] [Qed] Goal typed_cast_uchar_ensures : Valid
+[wp] Proved goals: 38 / 38
+ Qed: 34
Alt-Ergo: 4
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -55,4 +56,5 @@
band_bool 1 1 2 100%
bxor_bool 1 1 2 100%
lemma 7 - 7 100%
+ cast_uchar 1 - 1 100%
------------------------------------------------------------
--
GitLab