[wp] add vset testing

src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing vset.i (no preprocessing)
+[wp] Running WP plugin...
+------------------------------------------------------------
+  Global
+------------------------------------------------------------
+
+Goal Lemma 'direct_in':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Lemma 'indirect_equal_constants':
+Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
+  '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)))).
+
+------------------------------------------------------------
+
+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'
+Let a = L_Set2(int3_0, int2_0, int1_0).
+Assume {
+  Have: is_sint32(int1_0).
+  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) ->
+     ((i = int1_0) \/ (i = int2_0) \/ (i = int3_0)))).
+
+------------------------------------------------------------
+
+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'
+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'
+Prove: member(2, L_Set1).
+
+------------------------------------------------------------
+
+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'
+Assume { Have: is_sint32(int2_0). }
+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'
+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'
+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)).
+
+------------------------------------------------------------
+
+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'
+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)).
+
+------------------------------------------------------------
+
+Goal Lemma 'indirect_not_in_constants':
+Assume Lemmas: 'indirect_in_constants' 'direct_in'
+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'
+Prove: !member(0, L_Set3).
+
+------------------------------------------------------------
+
+Goal Lemma 'iota_compute_equal_constants':
+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'
+Let a = L_iota(4).
+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)))).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing vset.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 12 goals scheduled
+[wp] [Valid] typed_lemma_direct_in (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)
+[wp] [Valid] typed_lemma_indirect_in_constants (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_indirect_in_ghost (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_indirect_in_logical (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_indirect_not_equal_constants (Alt-Ergo) (Cached)
+[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
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     1       11       12       100%
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/vset.i

+
+//@ lemma direct_in: 2 \in {1,2,3};
+
+//@ logic set<integer> Set1 = {1,2,3};
+//@ lemma indirect_in_constants: 2 \in Set1;
+//@ lemma indirect_not_in_constants: ! (4 \in Set1);
+//@ lemma indirect_equal_constants: Set1 == {1,2,3};
+//@ lemma indirect_not_equal_constants: Set1 != {0,1,2};
+
+//@ logic integer i0 = 0;
+//@ logic integer i1 = 1;
+//@ logic integer i2 = 2;
+//@ logic integer i3 = 3;
+//@ logic set<integer> Set3 = {i1,i2,i3};
+//@ lemma indirect_in_logical: i2 \in Set3;
+//@ lemma indirect_not_in_logical: ! (i0 \in Set3);
+//@ lemma indirect_equal_logical: Set3 == {i1,i2,i3};
+//@ lemma indirect_not_equal_logical: Set3 != {i0,i1,i2};
+
+//@ ghost int int1 = 1;
+//@ ghost int int2 = 2;
+//@ ghost int int3 = 3;
+//@ logic set<int> Set2 = {int1,int2,int3};
+//@ lemma indirect_in_ghost: int2 \in Set2;
+//@ lemma indirect_equal_ghost: Set2 == {int1,int2,int3};
+
+/*@
+  logic set<integer> iota(integer n) =
+    (n <= 0) ? { 0 } : \union(n, iota(n-1)) ;
+
+  lemma iota_compute_equal_constants: iota(4) == { 0, 1, 2, 3, 4 };
+
+*/