From f7f5aeda0cd25f9db09d8282153b48dd89b4891f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Mar 2021 18:38:46 +0100
Subject: [PATCH] [wp] new test for post-assigns calls
---
.../wp_acsl/oracle/postassigns2.res.oracle | 24 +++++++++++++++++++
.../oracle_qualif/postassigns2.res.oracle | 14 +++++++++++
src/plugins/wp/tests/wp_acsl/postassigns2.c | 11 +++++++++
3 files changed, 49 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/postassigns2.c
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
new file mode 100644
index 00000000000..53e8b93a4eb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns2.res.oracle
@@ -0,0 +1,24 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function mess1
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_acsl/postassigns2.c, line 6) in 'mess1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns2.c, line 7) in 'mess1':
+Call Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns2.c, line 7) in 'mess1':
+Call Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
new file mode 100644
index 00000000000..e6a7ddd408d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns2.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns2.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_mess1_exits : Valid
+[wp] [Qed] Goal typed_mess1_assigns_exit : Valid
+[wp] [Qed] Goal typed_mess1_assigns_normal : Valid
+[wp] Proved goals: 3 / 3
+ Qed: 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ mess1 3 - 3 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/postassigns2.c b/src/plugins/wp/tests/wp_acsl/postassigns2.c
new file mode 100644
index 00000000000..eedaa11f4c3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/postassigns2.c
@@ -0,0 +1,11 @@
+/*@ exits \false;
+ @ assigns *(message + (0 .. \at(*\old(size),Post) - 1)), *size;
+*/
+void receive1(unsigned char *message, unsigned int *size);
+
+/*@ exits \false;
+ @ assigns *(message + (0 .. \at(*\old(size),Post) - 1)), *size;
+*/
+void mess1(unsigned char *message, unsigned int *size) {
+ receive1(message, size);
+}
--
GitLab