From 16c7e68ec466f11d3de3f2286252c855b29eef14 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Feb 2021 18:52:03 +0100
Subject: [PATCH] [wp] fixed cfg bugs
---
src/plugins/wp/tests/wp_plugin/cfg.c | 8 +++----
.../wp/tests/wp_plugin/oracle/cfg.res.oracle | 16 +++++++-------
.../wp_plugin/oracle_qualif/cfg.res.oracle | 21 +++++++++----------
3 files changed, 22 insertions(+), 23 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/cfg.c b/src/plugins/wp/tests/wp_plugin/cfg.c
index 0c0a510591c..76b6505c4cf 100644
--- a/src/plugins/wp/tests/wp_plugin/cfg.c
+++ b/src/plugins/wp/tests/wp_plugin/cfg.c
@@ -1,7 +1,7 @@
//@ assigns \nothing;
void foo(void);
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f1(void)
{
if (0 == 1)
@@ -14,7 +14,7 @@ void f1(void)
return_label: return;
}
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f1_simpler(void)
{
if (0 == 1)
@@ -26,7 +26,7 @@ void f1_simpler(void)
return_label: return;
}
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f1_variant(void)
{
if (0 == 1) L: ;
@@ -50,7 +50,7 @@ void f1_variant_invert(void)
return_label: return;
}
-/*@ ensures BUG_WP: \false; */
+/*@ ensures BUG_LEGACY_WP: \false; */
void f2(void)
{
if (0 == 1)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
index f78e97da034..7f60486d328 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cfg.res.oracle
@@ -6,24 +6,24 @@
Function f1
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f1':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f1':
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function f1_simpler
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f1_simpler':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f1_simpler':
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function f1_variant
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f1_variant':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f1_variant':
+Prove: false.
------------------------------------------------------------
------------------------------------------------------------
@@ -38,7 +38,7 @@ Prove: false.
Function f2
------------------------------------------------------------
-Goal Post-condition 'BUG_WP' in 'f2':
-Prove: true.
+Goal Post-condition 'BUG_LEGACY_WP' in 'f2':
+Prove: false.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
index 65a2d69e16b..9fc9c79a780 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/cfg.res.oracle
@@ -3,19 +3,18 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
-[wp] [Qed] Goal typed_f1_ensures_BUG_WP : Valid
-[wp] [Qed] Goal typed_f1_simpler_ensures_BUG_WP : Valid
-[wp] [Qed] Goal typed_f1_variant_ensures_BUG_WP : Valid
+[wp] [Alt-Ergo] Goal typed_f1_ensures_BUG_LEGACY_WP : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f1_simpler_ensures_BUG_LEGACY_WP : Unsuccess
+[wp] [Alt-Ergo] Goal typed_f1_variant_ensures_BUG_LEGACY_WP : Unsuccess
[wp] [Alt-Ergo] Goal typed_f1_variant_invert_ensures_FAILS_AS_EXPECTED : Unsuccess
-[wp] [Qed] Goal typed_f2_ensures_BUG_WP : Valid
-[wp] Proved goals: 4 / 5
- Qed: 4
- Alt-Ergo: 0 (unsuccess: 1)
+[wp] [Alt-Ergo] Goal typed_f2_ensures_BUG_LEGACY_WP : Unsuccess
+[wp] Proved goals: 0 / 5
+ Alt-Ergo: 0 (unsuccess: 5)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- f1 1 - 1 100%
- f1_simpler 1 - 1 100%
- f1_variant 1 - 1 100%
+ f1 - - 1 0.0%
+ f1_simpler - - 1 0.0%
+ f1_variant - - 1 0.0%
f1_variant_invert - - 1 0.0%
- f2 1 - 1 100%
+ f2 - - 1 0.0%
------------------------------------------------------------
--
GitLab