From 3f95b9a416df4a4c0f96096f25c733da34a474fd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 4 Oct 2024 10:27:20 +0200
Subject: [PATCH] [wp/region] swap tests
---
src/plugins/wp/tests/ptests_config | 16 +++--
.../wp/tests/wp_region/oracle/swap.res.oracle | 72 +++++++++++++++++++
.../wp_region/oracle_qualif/swap.res.oracle | 27 +++++++
src/plugins/wp/tests/wp_region/swap.i | 29 ++++++++
src/plugins/wp/tests/wp_region/test_config | 1 +
.../wp/tests/wp_region/test_config_qualif | 1 +
6 files changed, 140 insertions(+), 6 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/swap.i
create mode 100644 src/plugins/wp/tests/wp_region/test_config
create mode 100644 src/plugins/wp/tests/wp_region/test_config_qualif
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index 9ea351239b8..b70003f3d7c 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,8 +1,12 @@
-DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
-DEFAULT_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
+## General Purpose
+DEFAULT_SUITES= wp wp_manual wp_usage wp_plugin wp_gallery wp_tip wp_bts
+qualif_SUITES= wp wp_manual wp_usage wp_plugin wp_gallery wp_tip wp_bts
-qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
-qualif_SUITES= wp_typed wp_bytes wp_usage wp_gallery wp_manual wp_tip
-qualif_SUITES= why3
+## Memory Models
+DEFAULT_SUITES= wp_acsl wp_hoare wp_store wp_typed wp_bytes wp_region
+qualif_SUITES= wp_acsl wp_hoare wp_store wp_typed wp_bytes wp_region
-ce_SUITES= wp_ce
+## Specific Objectives
+qualif_SUITES= why3
+DEFAULT_SUITES= wp_ce
+ce_SUITES= wp_ce
diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
new file mode 100644
index 00000000000..e17459e0f2a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle
@@ -0,0 +1,72 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing swap.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal swap_aliased_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_aliased_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal swap_separated_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_separated_terminates (Cfg) (Trivial)
+------------------------------------------------------------
+ Function swap_aliased
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 20) in 'swap_aliased':
+Let a = ValueChunk_2[global(P_b_33)].
+Let a_1 = ValueChunk_1[global(P_a_32)].
+Let x = ValueChunk_0[a_1].
+Let x_1 = ValueChunk_0[a].
+Let x_2 = ValueChunk_0[a_1 <- x_1][a <- x][a_1].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2).
+ (* Heap *)
+ Type: linked(alloc_0) /\ framed(ValueChunk_1) /\ framed(ValueChunk_2).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, a_1, 4).
+ (* Pre-condition *)
+ Have: valid_rw(alloc_0, a, 4).
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 21) in 'swap_aliased':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 22) in 'swap_aliased' (1/2):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 22) in 'swap_aliased' (2/2):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function swap_separated
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 5) in 'swap_separated':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file swap.i, line 6) in 'swap_separated':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 7) in 'swap_separated' (1/2):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file swap.i, line 7) in 'swap_separated' (2/2):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
new file mode 100644
index 00000000000..3f2fc25aafc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle
@@ -0,0 +1,27 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing swap.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal swap_aliased_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_aliased_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] [Valid] Goal swap_separated_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal swap_separated_terminates (Cfg) (Trivial)
+[wp] 8 goals scheduled
+[wp] [Valid] region_swap_separated_ensures (Qed)
+[wp] [Valid] region_swap_separated_ensures_2 (Qed)
+[wp] [Valid] region_swap_separated_assigns_part1 (Qed)
+[wp] [Valid] region_swap_separated_assigns_part2 (Qed)
+[wp] [Valid] region_swap_aliased_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_swap_aliased_ensures_2 (Qed)
+[wp] [Valid] region_swap_aliased_assigns_part1 (Qed)
+[wp] [Valid] region_swap_aliased_assigns_part2 (Qed)
+[wp] Proved goals: 12 / 12
+ Terminating: 2
+ Unreachable: 2
+ Qed: 7
+ Alt-Ergo: 1
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ swap_separated 4 - 4 100%
+ swap_aliased 3 1 4 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/swap.i b/src/plugins/wp/tests/wp_region/swap.i
new file mode 100644
index 00000000000..04816ea5fd8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/swap.i
@@ -0,0 +1,29 @@
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region A: *a, B: *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_separated(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
+
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region R: *a, *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_aliased(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config
new file mode 100644
index 00000000000..87e39087d8a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/test_config
@@ -0,0 +1 @@
+OPT: -wp-model region
diff --git a/src/plugins/wp/tests/wp_region/test_config_qualif b/src/plugins/wp/tests/wp_region/test_config_qualif
new file mode 100644
index 00000000000..87e39087d8a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/test_config_qualif
@@ -0,0 +1 @@
+OPT: -wp-model region
--
GitLab