From bf5ffd5d61abcf91fbe3b88a5b6e2d6fc418a89c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 24 Sep 2020 15:27:49 +0200
Subject: [PATCH] [WP] Add tests for EVA model
---
.../wp/tests/wp_eva/oracle/simple.res.oracle | 34 +++++++++++++++++++
src/plugins/wp/tests/wp_eva/simple.c | 28 +++++++++++++++
src/plugins/wp/tests/wp_eva/test_config | 2 ++
3 files changed, 64 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_eva/oracle/simple.res.oracle
create mode 100644 src/plugins/wp/tests/wp_eva/simple.c
create mode 100644 src/plugins/wp/tests/wp_eva/test_config
diff --git a/src/plugins/wp/tests/wp_eva/oracle/simple.res.oracle b/src/plugins/wp/tests/wp_eva/oracle/simple.res.oracle
new file mode 100644
index 00000000000..92b9b4f7d77
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/oracle/simple.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing tests/wp_eva/simple.c (with preprocessing)
+[eva:alarm] tests/wp_eva/simple.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/wp_eva/simple.c:19: Warning: assertion got status unknown.
+[wp] Running WP plugin...
+[wp] tests/wp_eva/simple.c:28: Warning:
+ Ignored 'terminates' specification:
+ \false
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 14):
+Let x = read_sint32(MVar_z_0, 0).
+Let x_1 = 1 + x.
+Assume { Type: is_sint32(x) /\ is_sint32(x_1). }
+Prove: P_P(x_1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Assertion (file tests/wp_eva/simple.c, line 19):
+Let x = read_sint32(MVar_x_0, 0).
+Let x_1 = read_sint32(MVar_y_0, 0).
+Let x_2 = read_sint32(MVar_z_0, 0).
+Let x_3 = 1 + x.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
+}
+Prove: P_P(x_1) /\ P_P(x_2) /\ P_P(x_3).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_eva/simple.c b/src/plugins/wp/tests/wp_eva/simple.c
new file mode 100644
index 00000000000..4e5a58321e7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/simple.c
@@ -0,0 +1,28 @@
+#include "__fc_builtin.h"
+
+/*@
+ axiomatic P {
+ predicate P(int x);
+ }
+
+ @*/
+
+int z;
+
+void f (int *x, int *y){
+ *x = *x+1;
+ /*@ assert P(*x) && P(*y) && P(z); @*/
+}
+
+void g (int *x, int *y){
+ *x = *x+1;
+ /*@ assert P(*x) && P(*y) && P(z); @*/
+}
+
+void main(){
+ int x = Frama_C_interval(2,1000);
+ int y = Frama_C_interval(2,1000);
+ z = Frama_C_interval(2,1000);
+ f(&z,&z);
+ g(&x,&y);
+}
diff --git a/src/plugins/wp/tests/wp_eva/test_config b/src/plugins/wp/tests/wp_eva/test_config
new file mode 100644
index 00000000000..003797ac995
--- /dev/null
+++ b/src/plugins/wp/tests/wp_eva/test_config
@@ -0,0 +1,2 @@
+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 value
--
GitLab