From 6e8d16b9e151ddb83a2436176bfa98017e0e3992 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 18 Mar 2022 10:16:04 +0100
Subject: [PATCH] [wp] restores a test
---
src/plugins/wp/tests/wp_plugin/combined.c | 16 ++++++------
.../oracle_qualif/combined.res.oracle | 26 +++++++++++++++++++
2 files changed, 34 insertions(+), 8 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/combined.c b/src/plugins/wp/tests/wp_plugin/combined.c
index 3e0939d7e6c..5123a528dd6 100644
--- a/src/plugins/wp/tests/wp_plugin/combined.c
+++ b/src/plugins/wp/tests/wp_plugin/combined.c
@@ -1,15 +1,15 @@
/* run.config_qualif
- DONTRUN: [PB] temporary removed since a difference has to be validated.
-*/
-
-/* run.config_qualif
- MODULE: @PTEST_DIR@/@PTEST_NAME@
OPT: -wp-par 1
*/
-/* ZD : this should not be here such as it cannot be tested by all frama-c
- developer
- */
+
+
+
+
+
+
+
+
/*@ axiomatic A {
@ predicate P(int x);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle
new file mode 100644
index 00000000000..4cb64dc0e51
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/combined.res.oracle
@@ -0,0 +1,26 @@
+# frama-c -wp [...]
+[kernel] Parsing combined.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 14 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_assert : Unsuccess
+[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
+[wp] [Alt-Ergo] Goal typed_job_loop_invariant_2_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_2_established : Valid
+[wp] [Alt-Ergo] Goal typed_job_loop_invariant_3_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_3_established : Valid
+[wp] [Alt-Ergo] Goal typed_job_assert_2 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_2_part1 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_2_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_job_loop_assigns_2_part3 : Valid
+[wp] Proved goals: 13 / 14
+ Qed: 9
+ Alt-Ergo: 4 (unsuccess: 1)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 9 4 14 92.9%
+------------------------------------------------------------
--
GitLab