From d229ab908810331d482bd72e3b70aae597974094 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 3 Nov 2020 15:00:23 +0100
Subject: [PATCH] [wp] tests for post-assigns
---
.../wp_acsl/oracle/postassigns.res.oracle | 230 ++++++++++++++++++
.../oracle_qualif/postassigns.res.oracle | 65 +++++
src/plugins/wp/tests/wp_acsl/postassigns.c | 44 ++++
3 files changed, 339 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
create mode 100644 src/plugins/wp/tests/wp_acsl/postassigns.c
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
new file mode 100644
index 00000000000..8abc928d33f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/postassigns.res.oracle
@@ -0,0 +1,230 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function job1
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/postassigns.c, line 4) in 'job1':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (2/9):
+Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (3/9):
+Effect at line 10
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (4/9):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (5/9):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (6/9):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (7/9):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (8/9):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 5) in 'job1' (9/9):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function job2
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_acsl/postassigns.c, line 19) in 'job2':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (1/9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (2/9):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (3/9):
+Effect at line 25
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (4/9):
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (5/9):
+Effect at line 26
+Let x = A[1].
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ IsArray_sint32(A) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_sint32(p, x), 1).
+}
+Prove: exists i : Z. (A[i] = x) /\ (0 <= i) /\ (i <= 3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (6/9):
+Effect at line 27
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (7/9):
+Effect at line 27
+Let x = A[2].
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ IsArray_sint32(A) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, shift_sint32(p, x), 1).
+}
+Prove: exists i : Z. (A[i] = x) /\ (0 <= i) /\ (i <= 3).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (8/9):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 20) in 'job2' (9/9):
+Effect at line 28
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function job3
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_acsl/postassigns.c, line 38):
+Assume {
+ Type: is_sint32(N) /\ is_sint32(i) /\ is_sint32(1 + i).
+ (* Pre-condition *)
+ Have: 0 <= N.
+ (* Invariant *)
+ Have: (i <= N) /\ (0 <= i).
+ (* Then *)
+ Have: i < N.
+}
+Prove: (-1) <= i.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_acsl/postassigns.c, line 38):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (2/3):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/postassigns.c, line 39) (3/3):
+Effect at line 42
+Let a = shift_sint32(p, i).
+Assume {
+ Type: is_sint32(N) /\ is_sint32(i).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ linked(Malloc_0).
+ (* Goal *)
+ When: !invalid(Malloc_0, a, 1).
+ (* Pre-condition *)
+ Have: 0 <= N.
+ (* Invariant *)
+ Have: (i <= N) /\ (0 <= i).
+ (* Then *)
+ Have: i < N.
+}
+Prove: included(a, 1, shift_sint32(p, 0), N).
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 33) in 'job3' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_acsl/postassigns.c, line 33) in 'job3' (2/2):
+Effect at line 41
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_acsl/postassigns.c:7: Warning:
+ Memory model hypotheses for function 'job1':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post) - 1), &N);
+ */
+ void job1(int *p);
+[wp] tests/wp_acsl/postassigns.c:22: Warning:
+ Memory model hypotheses for function 'job2':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), (int *)A + (..), &N);
+ ensures \separated(p + A[0 .. \at(N,Post) - 1], (int *)A + (..), &N);
+ */
+ void job2(int *p);
+[wp] tests/wp_acsl/postassigns.c:35: Warning:
+ Memory model hypotheses for function 'job3':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post)), &N);
+ */
+ void job3(int *p);
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
new file mode 100644
index 00000000000..ef70c9d2f6e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/postassigns.res.oracle
@@ -0,0 +1,65 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/postassigns.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 27 goals scheduled
+[wp] [Qed] Goal typed_job1_ensures : Valid
+[wp] [Qed] Goal typed_job1_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part4 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part5 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part6 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part7 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part8 : Valid
+[wp] [Qed] Goal typed_job1_assigns_part9 : Valid
+[wp] [Qed] Goal typed_job2_ensures : Valid
+[wp] [Qed] Goal typed_job2_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part4 : Valid
+[wp] [Alt-Ergo] Goal typed_job2_assigns_part5 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part6 : Valid
+[wp] [Alt-Ergo] Goal typed_job2_assigns_part7 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part8 : Valid
+[wp] [Qed] Goal typed_job2_assigns_part9 : Valid
+[wp] [Alt-Ergo] Goal typed_job3_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job3_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_job3_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job3_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_job3_loop_assigns_part3 : Valid
+[wp] [Qed] Goal typed_job3_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job3_assigns_part2 : Valid
+[wp] Proved goals: 27 / 27
+ Qed: 23
+ Alt-Ergo: 4
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job1 10 - 10 100%
+ job2 8 2 10 100%
+ job3 5 2 7 100%
+------------------------------------------------------------
+[wp] tests/wp_acsl/postassigns.c:7: Warning:
+ Memory model hypotheses for function 'job1':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post) - 1), &N);
+ */
+ void job1(int *p);
+[wp] tests/wp_acsl/postassigns.c:22: Warning:
+ Memory model hypotheses for function 'job2':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), (int *)A + (..), &N);
+ ensures \separated(p + A[0 .. \at(N,Post) - 1], (int *)A + (..), &N);
+ */
+ void job2(int *p);
+[wp] tests/wp_acsl/postassigns.c:35: Warning:
+ Memory model hypotheses for function 'job3':
+ /*@
+ behavior wp_typed:
+ requires \separated(p + (..), &N);
+ ensures \separated(p + (0 .. \at(N,Post)), &N);
+ */
+ void job3(int *p);
diff --git a/src/plugins/wp/tests/wp_acsl/postassigns.c b/src/plugins/wp/tests/wp_acsl/postassigns.c
new file mode 100644
index 00000000000..a2c1b7d1ba8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/postassigns.c
@@ -0,0 +1,44 @@
+int N;
+
+/*@
+ ensures N == 4;
+ assigns N, p[0..\at(N,Post)-1];
+*/
+void job1(int *p)
+{
+ N = 0;
+ p[N++] = 0;
+ p[N++] = 0;
+ p[N++] = 0;
+ p[N++] = 0;
+}
+
+int A[4];
+
+/*@
+ ensures N == 4;
+ assigns N, *(p + A[0..\at(N,Post)-1]);
+*/
+void job2(int *p)
+{
+ N = 0;
+ p[A[N++]] = 0;
+ p[A[N++]] = 0;
+ p[A[N++]] = 0;
+ p[A[N++]] = 0;
+}
+
+/*@
+ requires 0 <= N;
+ assigns N, p[0..\at(N,Post)];
+*/
+void job3(int *p)
+{
+ /*@
+ loop invariant 0 <= i <= N;
+ loop assigns i, p[0..N-1];
+ */
+ for (int i = 0; i < N; i++)
+ p[i] = 0;
+ N++;
+}
--
GitLab