From d2dff38efb4ebec77c3d67ce57efedaecc823857 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 24 Sep 2020 22:55:33 +0200
Subject: [PATCH] [WP-Eva] Add a tests qualif
---
Makefile | 2 +-
.../wp_eva/oracle_qualif/simple.0.res.oracle | 26 +++++++++++++++++++
.../wp_eva/oracle_qualif/simple.1.res.oracle | 23 ++++++++++++++++
src/plugins/wp/tests/wp_eva/simple.c | 12 +++++++++
src/plugins/wp/tests/wp_eva/test_config | 4 +--
.../wp/tests/wp_eva/test_config_qualif | 2 ++
6 files changed, 65 insertions(+), 4 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_eva/test_config_qualif
diff --git a/Makefile b/Makefile
index add6a8e330e..fa0c654f9a9 100644
--- a/Makefile
+++ b/Makefile
@@ -945,7 +945,7 @@ PLUGIN_NAME:=Reduc
PLUGIN_DISTRIBUTED:=yes
PLUGIN_DIR:=src/plugins/reduc
PLUGIN_CMO:=reduc_options misc value2acsl collect hyp register
-PLUGIN_DEPENDENCIES:=Value
+PLUGIN_DEPENDENCIES:=Eva
$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
diff --git a/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
new file mode 100644
index 00000000000..0aceb023406
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.0.res.oracle
@@ -0,0 +1,26 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+# frama-c -wp -wp-model 'Eva1' [...]
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:34: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Alt-Ergo] Goal eva1_f_assert : Failed
+ [Why3 Error] Not a predicate symbol: write_sint32
+[wp] [Alt-Ergo] Goal eva1_f_assert_Eva_division_by_zero : Failed
+ [Why3 Error] Not a predicate symbol: write_sint321
+[wp] Failure: Undefined symbol 'read_sint32'
+[wp] [Alt-Ergo] Goal eva1_g_assert : Failed
+ [Why3 Error] anomaly: Log.AbortFatal("wp")
+[wp] Proved goals: 0 / 3
+ Alt-Ergo: 0 (failed: 3)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - - 2 0.0%
+ g - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
new file mode 100644
index 00000000000..21d94a667b9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle_qualif/simple.1.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:25: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:26: Warning:
+ division by zero. assert (int)(*x - 42) ≢ 0;
+[eva:alarm] tests/wp_eva/simple.c:31: Warning: assertion got status unknown.
+# frama-c -wp -wp-model 'Eva2' [...]
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:34: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Alt-Ergo] Goal eva2_f_assert : Timeout (missing cache)
+[wp] [Alt-Ergo] Goal eva2_f_assert_Eva_division_by_zero : Valid (missing cache)
+[wp] [Alt-Ergo] Goal eva2_g_assert : Timeout (missing cache)
+[wp] Proved goals: 1 / 3
+ Qed: 0
+ Alt-Ergo: 1 (unsuccess: 2)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f - 1 2 50.0%
+ g - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/simple.c b/src/plugins/wp/tests/wp_eva/simple.c
index 4e5a58321e7..728d2b49d2a 100644
--- a/src/plugins/wp/tests/wp_eva/simple.c
+++ b/src/plugins/wp/tests/wp_eva/simple.c
@@ -1,3 +1,13 @@
+/* run.config
+ OPT: -wp-model eva1
+ OPT: -wp-model eva2
+*/
+
+/* run.config_qualif
+ OPT: -wp-model eva1
+ OPT: -wp-model eva2
+*/
+
#include "__fc_builtin.h"
/*@
@@ -10,8 +20,10 @@
int z;
void f (int *x, int *y){
+ if(z==41) return;
*x = *x+1;
/*@ assert P(*x) && P(*y) && P(z); @*/
+ int r = 1/(*x-42);
}
void g (int *x, int *y){
diff --git a/src/plugins/wp/tests/wp_eva/test_config b/src/plugins/wp/tests/wp_eva/test_config
index c01e5325329..8b6102546cc 100644
--- a/src/plugins/wp/tests/wp_eva/test_config
+++ b/src/plugins/wp/tests/wp_eva/test_config
@@ -1,3 +1 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope -eva -load-module wp -eva-no-print -eva-verbose 0
-OPT: -then -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell -wp-model eva1
-OPT: -then -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell -wp-model eva2
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -wp -wp-print -wp-prover none -wp-share ./share -wp-msg-key shell
diff --git a/src/plugins/wp/tests/wp_eva/test_config_qualif b/src/plugins/wp/tests/wp_eva/test_config_qualif
new file mode 100644
index 00000000000..153e5ddde39
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/test_config_qualif
@@ -0,0 +1,2 @@
+CMD: @frama-c@ -no-autoload-plugins -load-module eva,scope,reduc,wp -eva -eva-no-print -eva-verbose 0 @PTEST_FILE@ -then -reduc -reduc-gen-annot all -then -no-reduc -then -wp -wp-par 1 -wp-share ./share -wp-msg-key shell -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache-env -wp-cache replay @PTEST_FILE@ -wp-coq-timeout 120
+OPT:
--
GitLab