Skip to content
Snippets Groups Projects
Commit c91d2a7e authored by Cécile Ruet-Cros's avatar Cécile Ruet-Cros
Browse files

[wp] vset: add options for tests

parent e54e0a67
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
+ 43
− 14
View file @ c91d2a7e
# frama-c -wp [...]
[kernel] Parsing vset.i (no preprocessing)
[wp] Running WP plugin...
[wp] 21 goals scheduled
[wp] [Valid] typed_lemma_direct_in (Qed)
[wp] [Valid] typed_lemma_direct_in_singleton (Qed)
[wp] [NoResult] typed_lemma_indirect_in_constants (Qed)
[wp] [Unsuccess] typed_lemma_indirect_equal_logical (Tactic) (Qed)
[wp] [Unsuccess] typed_lemma_indirect_equal_ghost (Tactic) (Qed)
[wp] [Unsuccess] typed_lemma_indirect_equal_constants (Tactic) (Qed)
[wp] [NoResult] typed_lemma_indirect_not_equal_logical (Qed)
[wp] [NoResult] typed_lemma_indirect_not_equal_constants (Qed)
[wp] [NoResult] typed_lemma_indirect_in_logical (Qed)
[wp] [NoResult] typed_lemma_indirect_in_ghost (Qed)
[wp] [Unsuccess] typed_lemma_iota1_compute_equal_constants (Tactic) (Qed)
[wp] [NoResult] typed_lemma_iota0_compute_0in_constants (Qed)
[wp] [NoResult] typed_lemma_indirect_not_in_logical (Qed)
[wp] [NoResult] typed_lemma_indirect_not_in_constants (Qed)
[wp] [Unsuccess] typed_lemma_iota_ind0 (Tactic) (Qed)
[wp] [Unsuccess] typed_lemma_iota3_compute_equal_constants (Tactic) (Qed)
[wp] [NoResult] typed_lemma_iota3_compute_2in_constants (Qed)
[wp] [NoResult] typed_lemma_iota3_compute_0in_constants (Qed)
[wp] [NoResult] typed_lemma_rec_iota_le0 (Qed)
[wp] [NoResult] typed_lemma_rec_iota_gt0 (Qed)
[wp] [NoResult] typed_lemma_rec_iota (Qed)
[wp] Proved goals: 2 / 21
Qed: 2
Unsuccess: 19
Missing: 13
------------------------------------------------------------
Global
------------------------------------------------------------
Goal Lemma 'direct_in':
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Lemma 'direct_in_singleton':
Assume Lemmas: 'direct_in'
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
......@@ -21,6 +49,7 @@ Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
'direct_in_singleton' 'direct_in'
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)))).
Prover Script returns Unsuccess
------------------------------------------------------------
......@@ -30,15 +59,11 @@ Assume Lemmas: 'indirect_in_ghost' 'indirect_not_equal_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
'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).
Have: is_sint32(int2_0).
Have: is_sint32(int3_0).
}
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)))).
Let a = L_Set2(int2_0, int1_0).
Assume { Have: is_sint32(int1_0). Have: is_sint32(int2_0). }
Prove: mem(int1_0, a) /\ mem(int2_0, a) /\
(forall i : Z. (mem(i, a) -> ((i = int1_0) \/ (i = int2_0)))).
Prover Script returns Unsuccess
------------------------------------------------------------
......@@ -47,8 +72,9 @@ 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: 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)))).
Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\
(forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2)))).
Prover Script returns Unsuccess
------------------------------------------------------------
......@@ -65,7 +91,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: mem(int2_0, L_Set2(int3_0, int2_0, int1_0)).
Prove: mem(int2_0, L_Set2(int2_0, int1_0)).
------------------------------------------------------------
......@@ -90,8 +116,8 @@ 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: (!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)).
Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/
(exists i : Z. (i != 0) /\ (i != 1) /\ mem(i, L_Set3)).
------------------------------------------------------------
......@@ -132,6 +158,7 @@ Assume Lemmas: 'iota3_compute_equal_constants' 'iota3_compute_2in_constants'
Let a = L_iota(1).
Prove: mem(0, a) /\ mem(1, a) /\
(forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1)))).
Prover Script returns Unsuccess
------------------------------------------------------------
......@@ -171,6 +198,7 @@ Assume Lemmas: 'iota3_compute_2in_constants' 'iota3_compute_0in_constants'
Let a = L_iota(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)))).
Prover Script returns Unsuccess
------------------------------------------------------------
......@@ -183,6 +211,7 @@ Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
'direct_in'
Let a = L_iota(n). Assume { Have: n <= 0. }
Prove: mem(0, a) /\ (forall i : Z. (mem(i, a) -> (i = 0))).
Prover Script returns Unsuccess
------------------------------------------------------------
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
+ 6
− 6
View file @ c91d2a7e
......@@ -18,16 +18,16 @@
[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_iota3_compute_equal_constants (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_lemma_iota_ind0 (Tactic) (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
[wp] Proved goals: 19 / 21
Qed: 2
Alt-Ergo: 16
Unsuccess: 3
Alt-Ergo: 17
Unsuccess: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma 2 16 21 85.7%
Lemma 2 17 21 90.5%
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/vset.i
+ 11
− 7
View file @ c91d2a7e
/* run.config
OPT:-wp-auto wp:split
*/
/* run.config_qualif
OPT:-wp-auto wp:split
*/
//@ lemma direct_in: 2 \in {1,2,3};
//@ lemma direct_in_singleton: 2 \in {2};
......@@ -11,19 +17,17 @@
//@ logic integer i0 = 0;
//@ logic integer i1 = 1;
//@ logic integer i2 = 2;
//@ logic integer i3 = 3;
//@ logic set<integer> Set3 = {i1,i2,i3};
//@ logic set<integer> Set3 = {i1,i2};
//@ 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};
//@ lemma indirect_equal_logical: Set3 == {i1,i2};
//@ lemma indirect_not_equal_logical: Set3 != {i0,i1};
//@ ghost int int1 = 1;
//@ ghost int int2 = 2;
//@ ghost int int3 = 3;
//@ logic set<int> Set2 = {int1,int2,int3};
//@ logic set<int> Set2 = {int1,int2};
//@ lemma indirect_in_ghost: int2 \in Set2;
//@ lemma indirect_equal_ghost: Set2 == {int1,int2,int3};
//@ lemma indirect_equal_ghost: Set2 == {int1,int2};
/*@
logic set<integer> iota(integer n) =
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment