From e54e0a670cf93deaeaa9e9c61d8b323562851564 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 16:19:45 +0200
Subject: [PATCH] [wp] vset add test oracles
---
src/plugins/wp/share/why3/frama_c_wp/vset.mlw | 20 +++----
.../wp/tests/wp_acsl/oracle/vset.res.oracle | 59 +++++++++----------
2 files changed, 38 insertions(+), 41 deletions(-)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
index 65e6de7179d..af94135774d 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/vset.mlw
@@ -36,7 +36,7 @@ theory Vset
function member_bool 'a (set 'a) : bool
predicate eqset (a : set 'a) (b : set 'a) =
- forall x : 'a. (member x a) <-> (member x b)
+ forall x : 'a. (mem x a) <-> (mem x b)
function range int int : set int (* [a..b] *)
function range_sup int : set int (* [a..] *)
@@ -46,19 +46,19 @@ theory Vset
(* -------------------------------------------------------------------------- *)
axiom member_bool : forall x:'a. forall s:set 'a [member_bool x s].
- if member x s then member_bool x s = True else member_bool x s = False
+ if mem x s then member_bool x s = True else member_bool x s = False
- axiom member_range : forall x:int,a:int,b:int [member x (range a b)].
- member x (range a b) <-> (a <= x /\ x <= b)
+ axiom member_range : forall x:int,a:int,b:int [mem x (range a b)].
+ mem x (range a b) <-> (a <= x /\ x <= b)
- axiom member_range_sup : forall x:int,a:int [member x (range_sup a)].
- member x (range_sup a) <-> (a <= x)
+ axiom member_range_sup : forall x:int,a:int [mem x (range_sup a)].
+ mem x (range_sup a) <-> (a <= x)
- axiom member_range_inf : forall x:int,b:int [member x (range_inf b)].
- member x (range_inf b) <-> (x <= b)
+ axiom member_range_inf : forall x:int,b:int [mem x (range_inf b)].
+ mem x (range_inf b) <-> (x <= b)
- axiom member_range_all : forall x:int [member x range_all].
- member x range_all
+ axiom member_range_all : forall x:int [mem x range_all].
+ mem x range_all
(* -------------------------------------------------------------------------- *)
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 110faf822ca..a71978a9753 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
@@ -19,8 +19,8 @@ Prove: true.
Goal Lemma 'indirect_equal_constants':
Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
'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)))).
+Prove: mem(1, L_Set1) /\ mem(2, L_Set1) /\ mem(3, L_Set1) /\
+ (forall i : Z. (mem(i, L_Set1) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
------------------------------------------------------------
@@ -36,8 +36,8 @@ Assume {
Have: is_sint32(int2_0).
Have: is_sint32(int3_0).
}
-Prove: member(int1_0, a) /\ member(int2_0, a) /\ member(int3_0, a) /\
- (forall i : Z. (member(i, a) ->
+Prove: mem(int1_0, a) /\ mem(int2_0, a) /\ mem(int3_0, a) /\
+ (forall i : Z. (mem(i, a) ->
((i = int1_0) \/ (i = int2_0) \/ (i = int3_0)))).
------------------------------------------------------------
@@ -47,14 +47,14 @@ 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_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)))).
+Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\ mem(3, L_Set3) /\
+ (forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
------------------------------------------------------------
Goal Lemma 'indirect_in_constants':
Assume Lemmas: 'direct_in_singleton' 'direct_in'
-Prove: member(2, L_Set1).
+Prove: mem(2, L_Set1).
------------------------------------------------------------
@@ -65,7 +65,7 @@ Assume Lemmas: 'indirect_not_equal_logical' 'indirect_equal_logical'
'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)).
+Prove: mem(int2_0, L_Set2(int3_0, int2_0, int1_0)).
------------------------------------------------------------
@@ -73,16 +73,15 @@ Goal Lemma 'indirect_in_logical':
Assume Lemmas: 'indirect_not_equal_constants' 'indirect_equal_constants'
'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
'direct_in'
-Prove: member(2, L_Set3).
+Prove: mem(2, L_Set3).
------------------------------------------------------------
Goal Lemma 'indirect_not_equal_constants':
Assume Lemmas: 'indirect_equal_constants' 'indirect_not_in_constants'
'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)).
+Prove: (!mem(0, L_Set1)) \/ (!mem(1, L_Set1)) \/ (!mem(2, L_Set1)) \/
+ (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ mem(i, L_Set1)).
------------------------------------------------------------
@@ -91,15 +90,14 @@ 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_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)).
+Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/ (!mem(2, L_Set3)) \/
+ (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ mem(i, L_Set3)).
------------------------------------------------------------
Goal Lemma 'indirect_not_in_constants':
Assume Lemmas: 'indirect_in_constants' 'direct_in_singleton' 'direct_in'
-Prove: !member(4, L_Set1).
+Prove: !mem(4, L_Set1).
------------------------------------------------------------
@@ -107,7 +105,7 @@ 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_singleton' 'direct_in'
-Prove: !member(0, L_Set3).
+Prove: !mem(0, L_Set3).
------------------------------------------------------------
@@ -118,7 +116,7 @@ Assume Lemmas: 'rec_iota' 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
'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)).
+Prove: mem(0, L_iota(0)).
------------------------------------------------------------
@@ -132,8 +130,8 @@ Assume Lemmas: 'iota3_compute_equal_constants' 'iota3_compute_2in_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)))).
+Prove: mem(0, a) /\ mem(1, a) /\
+ (forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1)))).
------------------------------------------------------------
@@ -145,7 +143,7 @@ Assume Lemmas: 'iota0_compute_0in_constants' 'rec_iota' 'rec_iota_gt0'
'indirect_not_equal_constants' 'indirect_equal_constants'
'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
'direct_in'
-Prove: member(0, L_iota(3)).
+Prove: mem(0, L_iota(3)).
------------------------------------------------------------
@@ -157,7 +155,7 @@ Assume Lemmas: 'iota3_compute_0in_constants' 'iota0_compute_0in_constants'
'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)).
+Prove: mem(2, L_iota(3)).
------------------------------------------------------------
@@ -171,9 +169,8 @@ Assume Lemmas: 'iota3_compute_2in_constants' 'iota3_compute_0in_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) /\
- (forall i : Z. (member(i, a) ->
- ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3)))).
+Prove: mem(0, a) /\ mem(1, a) /\ mem(2, a) /\ mem(3, a) /\
+ (forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3)))).
------------------------------------------------------------
@@ -185,7 +182,7 @@ Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
'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))).
+Prove: mem(0, a) /\ (forall i : Z. (mem(i, a) -> (i = 0))).
------------------------------------------------------------
@@ -196,8 +193,8 @@ Assume Lemmas: 'rec_iota_gt0' 'rec_iota_le0' 'iota_ind0'
'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)).
+Assume { Have: mem(i, L_iota(n)). }
+Prove: (n = i) \/ mem(i, L_iota(n - 1)).
------------------------------------------------------------
@@ -208,8 +205,8 @@ Assume Lemmas: 'rec_iota_le0' 'iota_ind0' 'indirect_equal_ghost'
'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)).
+Assume { Have: 0 < n. Have: mem(i, L_iota(n)). }
+Prove: (n = i) \/ mem(i, L_iota(n - 1)).
------------------------------------------------------------
@@ -220,7 +217,7 @@ Assume Lemmas: 'iota_ind0' 'indirect_equal_ghost' 'indirect_in_ghost'
'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)). }
+Assume { Have: n <= 0. Have: mem(i, L_iota(n)). }
Prove: i = 0.
------------------------------------------------------------
--
GitLab