From 08516dfaeae8e312c60268a9784f8dbc82241505 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Tue, 8 Oct 2024 11:03:07 +0200
Subject: [PATCH] [wp/region] test + oracles
---
src/plugins/wp/tests/wp_region/affectations.c | 22 +++++
.../wp/tests/wp_region/heterogenous_cast.c | 10 +++
.../wp_region/oracle/affectations.res.oracle | 86 +++++++++++++++++++
.../oracle/heterogenous_cast.res.oracle | 85 ++++++++++++++++++
.../oracle_qualif/affectations.res.oracle | 22 +++++
.../heterogenous_cast.res.oracle | 65 ++++++++++++++
6 files changed, 290 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_region/affectations.c
create mode 100644 src/plugins/wp/tests/wp_region/heterogenous_cast.c
create mode 100644 src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
diff --git a/src/plugins/wp/tests/wp_region/affectations.c b/src/plugins/wp/tests/wp_region/affectations.c
new file mode 100644
index 00000000000..601aa47036e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/affectations.c
@@ -0,0 +1,22 @@
+/*@ predicate pointed(int *p, int* q) = p==q || \separated(p,q);
+*/
+
+/*@
+ requires \valid(p);
+ requires \valid(q);
+ requires pointed(p,q);
+ assigns *p, *q;
+ region PQ: *p, *q;
+ behavior EQ:
+ assumes p == q;
+ ensures P: *p == \old(*p);
+ ensures Q: *q == \old(*q);
+ behavior SEP:
+ assumes p != q;
+ ensures Q: *p == \old(*p)+1;
+ ensures Q: *q == \old(*q)-1;
+*/
+void f(int* p, int* q) {
+ (*p)++;
+ (*q)--;
+}
diff --git a/src/plugins/wp/tests/wp_region/heterogenous_cast.c b/src/plugins/wp/tests/wp_region/heterogenous_cast.c
new file mode 100644
index 00000000000..ef9c1c52cfb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/heterogenous_cast.c
@@ -0,0 +1,10 @@
+/*@
+ assigns *p;
+@*/
+void g (int *p) {
+ *p = 42;
+ short *q = (short*) p;
+ q[0] = -1;
+ q[1] = -1;
+ //@ assert *p == -1;
+}
diff --git a/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle b/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
new file mode 100644
index 00000000000..90b845e9227
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle
@@ -0,0 +1,86 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (1/2):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (2/2):
+Effect at line 21
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior EQ
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'P' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'Q' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function f with behavior SEP
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = 1 + x.
+Let m = Msint32_0[p <- x_1].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Let x_4 = m[q <- x_3][p].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(Msint32_0[q]) /\ is_sint32(x_2) /\
+ is_sint32(x_3) /\ is_sint32(x_4).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, p, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, q, 4).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Pre-condition for 'SEP' *)
+ Have: q != p.
+}
+Prove: x_4 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = Msint32_0[q].
+Let m = Msint32_0[p <- 1 + x].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+ is_sint32(m[q <- x_3][p]).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, p, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, q, 4).
+ (* Pre-condition *)
+ Have: P_pointed(p, q).
+ (* Pre-condition for 'SEP' *)
+ Have: q != p.
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
new file mode 100644
index 00000000000..f7b3f9e10a0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle
@@ -0,0 +1,85 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function g
+------------------------------------------------------------
+
+Goal Assertion (file heterogenous_cast.c, line 9):
+Let x = read_sint32(write_sint16(write_sint16(write_sint32(mem_0, p, 42),
+ shift_sint16(p, 0), -1),
+ shift_sint16(p, 1), -1), p).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (1/3):
+Effect at line 5
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (2/3):
+Effect at line 7
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (3/3):
+Effect at line 8
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
new file mode 100644
index 00000000000..3679fc28e57
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Valid] region_f_assigns_part1 (Qed)
+[wp] [Valid] region_f_assigns_part2 (Qed)
+[wp] [Valid] region_f_EQ_ensures_P (Qed)
+[wp] [Valid] region_f_EQ_ensures_Q (Qed)
+[wp] [Valid] region_f_SEP_ensures_Q (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_SEP_ensures_Q_2 (Alt-Ergo) (Cached)
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
+ Qed: 4
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 4 2 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
new file mode 100644
index 00000000000..5ef48e91de1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle
@@ -0,0 +1,65 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[wp] 4 goals scheduled
+[wp] [Valid] region_g_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_g_assigns_part1 (Qed)
+[wp] [Valid] region_g_assigns_part2 (Qed)
+[wp] [Valid] region_g_assigns_part3 (Qed)
+[wp] Proved goals: 6 / 6
+ Terminating: 1
+ Unreachable: 1
+ Qed: 3
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ g 3 1 4 100%
+------------------------------------------------------------
--
GitLab