From 88196f7ae9aff802ea7daa32b134992dcb0f32e5 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 26 Jul 2019 10:36:30 +0200
Subject: [PATCH] [libC] fixes specification of abort and exit functions:
adding a test for wp plugin
---
src/plugins/wp/tests/wp_bts/issue-684-exit.c | 8 ++++++
.../wp_bts/oracle/issue-684-exit.res.oracle | 28 +++++++++++++++++++
.../issue-684-exit.0.report.json | 22 +++++++++++++++
.../oracle_qualif/issue-684-exit.res.oracle | 18 ++++++++++++
4 files changed, 76 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_bts/issue-684-exit.c
create mode 100644 src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
diff --git a/src/plugins/wp/tests/wp_bts/issue-684-exit.c b/src/plugins/wp/tests/wp_bts/issue-684-exit.c
new file mode 100644
index 00000000000..9776a399902
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue-684-exit.c
@@ -0,0 +1,8 @@
+#include "stdlib.h"
+/*@ assigns \nothing;
+ @ exits \exit_status == state;
+ @ ensures \false;
+*/
+void inconditional_exit(int state) {
+ exit (state);
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
new file mode 100644
index 00000000000..2b2e6c21c2d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue-684-exit.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function inconditional_exit
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue-684-exit.c, line 4) in 'inconditional_exit':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Exit-condition (file tests/wp_bts/issue-684-exit.c, line 3) in 'inconditional_exit':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'inconditional_exit':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'inconditional_exit':
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json
new file mode 100644
index 00000000000..43d68882c15
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json
@@ -0,0 +1,22 @@
+{ "wp:global": { "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 4, "valid": 4 } },
+ "wp:functions": { "inconditional_exit": { "inconditional_exit_assigns":
+ { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "inconditional_exit_ensures":
+ { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "inconditional_exit_exits":
+ { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main":
+ { "total": 4,
+ "valid": 4 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
new file mode 100644
index 00000000000..798f9dce70e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-684-exit.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue-684-exit.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Qed] Goal typed_inconditional_exit_ensures : Valid
+[wp] [Qed] Goal typed_inconditional_exit_exits : Valid
+[wp] [Qed] Goal typed_inconditional_exit_assigns_exit : Valid
+[wp] [Qed] Goal typed_inconditional_exit_assigns_normal : Valid
+[wp] Proved goals: 4 / 4
+ Qed: 4
+[wp] Report in: 'tests/wp_bts/oracle_qualif/issue-684-exit.0.report.json'
+[wp] Report out: 'tests/wp_bts/result_qualif/issue-684-exit.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+inconditional_exit 4 - 4 100%
+-------------------------------------------------------------
--
GitLab