From 526c153ef60f46877059895df9c0e7d2f3707b94 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20Ruet-Cros?= <cecile.ruet-cros@cea.fr>
Date: Wed, 3 Jul 2024 14:48:38 +0200
Subject: [PATCH] [wp] update test oracles
---
.../wp/tests/wp_acsl/oracle/vset.res.oracle | 142 ++++++++++++++++--
.../wp_acsl/oracle_qualif/vset.res.oracle | 22 ++-
2 files changed, 142 insertions(+), 22 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
index 64a5e103aaa..110faf822ca 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
@@ -10,9 +10,15 @@ Prove: true.
------------------------------------------------------------
+Goal Lemma 'direct_in_singleton':
+Assume Lemmas: 'direct_in'
+Prove: true.
+
+------------------------------------------------------------
+
Goal Lemma 'indirect_equal_constants':
Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
- 'direct_in'
+ 'direct_in_singleton' 'direct_in'
Prove: member(1, L_Set1) /\ member(2, L_Set1) /\ member(3, L_Set1) /\
(forall i : Z. (member(i, L_Set1) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
@@ -22,7 +28,8 @@ Goal Lemma 'indirect_equal_ghost':
Assume Lemmas: 'indirect_in_ghost' 'indirect_not_equal_logical'
'indirect_equal_logical' 'indirect_not_in_logical' 'indirect_in_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
- 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
Let a = L_Set2(int3_0, int2_0, int1_0).
Assume {
Have: is_sint32(int1_0).
@@ -38,14 +45,15 @@ Prove: member(int1_0, a) /\ member(int2_0, a) /\ member(int3_0, a) /\
Goal Lemma 'indirect_equal_logical':
Assume Lemmas: 'indirect_not_in_logical' 'indirect_in_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
- 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
Prove: member(1, L_Set3) /\ member(2, L_Set3) /\ member(3, L_Set3) /\
(forall i : Z. (member(i, L_Set3) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
------------------------------------------------------------
Goal Lemma 'indirect_in_constants':
-Assume Lemmas: 'direct_in'
+Assume Lemmas: 'direct_in_singleton' 'direct_in'
Prove: member(2, L_Set1).
------------------------------------------------------------
@@ -54,7 +62,8 @@ Goal Lemma 'indirect_in_ghost':
Assume Lemmas: 'indirect_not_equal_logical' 'indirect_equal_logical'
'indirect_not_in_logical' 'indirect_in_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
- 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
Assume { Have: is_sint32(int2_0). }
Prove: member(int2_0, L_Set2(int3_0, int2_0, int1_0)).
@@ -62,14 +71,15 @@ Prove: member(int2_0, L_Set2(int3_0, int2_0, int1_0)).
Goal Lemma 'indirect_in_logical':
Assume Lemmas: 'indirect_not_equal_constants' 'indirect_equal_constants'
- 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
Prove: member(2, L_Set3).
------------------------------------------------------------
Goal Lemma 'indirect_not_equal_constants':
Assume Lemmas: 'indirect_equal_constants' 'indirect_not_in_constants'
- 'indirect_in_constants' 'direct_in'
+ 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
Prove: (!member(0, L_Set1)) \/ (!member(1, L_Set1)) \/
(!member(2, L_Set1)) \/
(exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ member(i, L_Set1)).
@@ -80,7 +90,7 @@ Goal Lemma 'indirect_not_equal_logical':
Assume Lemmas: 'indirect_equal_logical' 'indirect_not_in_logical'
'indirect_in_logical' 'indirect_not_equal_constants'
'indirect_equal_constants' 'indirect_not_in_constants'
- 'indirect_in_constants' 'direct_in'
+ 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
Prove: (!member(0, L_Set3)) \/ (!member(1, L_Set3)) \/
(!member(2, L_Set3)) \/
(exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ member(i, L_Set3)).
@@ -88,7 +98,7 @@ Prove: (!member(0, L_Set3)) \/ (!member(1, L_Set3)) \/
------------------------------------------------------------
Goal Lemma 'indirect_not_in_constants':
-Assume Lemmas: 'indirect_in_constants' 'direct_in'
+Assume Lemmas: 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
Prove: !member(4, L_Set1).
------------------------------------------------------------
@@ -96,21 +106,121 @@ Prove: !member(4, L_Set1).
Goal Lemma 'indirect_not_in_logical':
Assume Lemmas: 'indirect_in_logical' 'indirect_not_equal_constants'
'indirect_equal_constants' 'indirect_not_in_constants'
- 'indirect_in_constants' 'direct_in'
+ 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
Prove: !member(0, L_Set3).
------------------------------------------------------------
-Goal Lemma 'iota_compute_equal_constants':
-Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
+Goal Lemma 'iota0_compute_0in_constants':
+Assume Lemmas: 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
+ 'indirect_equal_ghost' 'indirect_in_ghost' 'indirect_not_equal_logical'
+ 'indirect_equal_logical' 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Prove: member(0, L_iota(0)).
+
+------------------------------------------------------------
+
+Goal Lemma 'iota1_compute_equal_constants':
+Assume Lemmas: 'iota3_compute_equal_constants' 'iota3_compute_2in_constants'
+ 'iota3_compute_0in_constants' 'iota0_compute_0in_constants' 'rec_iota'
+ 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
+ 'indirect_in_ghost' 'indirect_not_equal_logical' 'indirect_equal_logical'
+ 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Let a = L_iota(1).
+Prove: member(0, a) /\ member(1, a) /\
+ (forall i : Z. (member(i, a) -> ((i = 0) \/ (i = 1)))).
+
+------------------------------------------------------------
+
+Goal Lemma 'iota3_compute_0in_constants':
+Assume Lemmas: 'iota0_compute_0in_constants' 'rec_iota' 'rec_iota_gt0'
+ 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
'indirect_not_equal_logical' 'indirect_equal_logical'
'indirect_not_in_logical' 'indirect_in_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
- 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in'
-Let a = L_iota(4).
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Prove: member(0, L_iota(3)).
+
+------------------------------------------------------------
+
+Goal Lemma 'iota3_compute_2in_constants':
+Assume Lemmas: 'iota3_compute_0in_constants' 'iota0_compute_0in_constants'
+ 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
+ 'indirect_in_ghost' 'indirect_not_equal_logical' 'indirect_equal_logical'
+ 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Prove: member(2, L_iota(3)).
+
+------------------------------------------------------------
+
+Goal Lemma 'iota3_compute_equal_constants':
+Assume Lemmas: 'iota3_compute_2in_constants' 'iota3_compute_0in_constants'
+ 'iota0_compute_0in_constants' 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0'
+ 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
+ 'indirect_not_equal_logical' 'indirect_equal_logical'
+ 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Let a = L_iota(3).
Prove: member(0, a) /\ member(1, a) /\ member(2, a) /\ member(3, a) /\
- member(4, a) /\
(forall i : Z. (member(i, a) ->
- ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3) \/ (i = 4)))).
+ ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3)))).
+
+------------------------------------------------------------
+
+Goal Lemma 'iota_ind0':
+Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
+ 'indirect_not_equal_logical' 'indirect_equal_logical'
+ 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Let a = L_iota(n). Assume { Have: n <= 0. }
+Prove: member(0, a) /\ (forall i : Z. (member(i, a) -> (i = 0))).
+
+------------------------------------------------------------
+
+Goal Lemma 'rec_iota':
+Assume Lemmas: 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
+ 'indirect_equal_ghost' 'indirect_in_ghost' 'indirect_not_equal_logical'
+ 'indirect_equal_logical' 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Assume { Have: member(i, L_iota(n)). }
+Prove: (n = i) \/ member(i, L_iota(n - 1)).
+
+------------------------------------------------------------
+
+Goal Lemma 'rec_iota_gt0':
+Assume Lemmas: 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
+ 'indirect_in_ghost' 'indirect_not_equal_logical' 'indirect_equal_logical'
+ 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Assume { Have: 0 < n. Have: member(i, L_iota(n)). }
+Prove: (n = i) \/ member(i, L_iota(n - 1)).
+
+------------------------------------------------------------
+
+Goal Lemma 'rec_iota_le0':
+Assume Lemmas: 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
+ 'indirect_not_equal_logical' 'indirect_equal_logical'
+ 'indirect_not_in_logical' 'indirect_in_logical'
+ 'indirect_not_equal_constants' 'indirect_equal_constants'
+ 'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
+ 'direct_in'
+Assume { Have: n <= 0. Have: member(i, L_iota(n)). }
+Prove: i = 0.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
index 590587b0d95..f8daf4ebd2e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
@@ -1,8 +1,9 @@
# frama-c -wp [...]
[kernel] Parsing vset.i (no preprocessing)
[wp] Running WP plugin...
-[wp] 12 goals scheduled
+[wp] 21 goals scheduled
[wp] [Valid] typed_lemma_direct_in (Qed)
+[wp] [Valid] typed_lemma_direct_in_singleton (Qed)
[wp] [Valid] typed_lemma_indirect_equal_constants (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_indirect_equal_ghost (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_indirect_equal_logical (Alt-Ergo) (Cached)
@@ -13,11 +14,20 @@
[wp] [Valid] typed_lemma_indirect_not_equal_logical (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_indirect_not_in_constants (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_indirect_not_in_logical (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_iota_compute_equal_constants (Alt-Ergo) (Cached)
-[wp] Proved goals: 12 / 12
- Qed: 1
- Alt-Ergo: 11
+[wp] [Valid] typed_lemma_iota0_compute_0in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_iota1_compute_equal_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_iota3_compute_0in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_iota3_compute_2in_constants (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_lemma_iota3_compute_equal_constants (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_lemma_iota_ind0 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_rec_iota (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_lemma_rec_iota_gt0 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_rec_iota_le0 (Alt-Ergo) (Cached)
+[wp] Proved goals: 18 / 21
+ Qed: 2
+ Alt-Ergo: 16
+ Unsuccess: 3
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma 1 11 12 100%
+ Lemma 2 16 21 85.7%
------------------------------------------------------------
--
GitLab