diff --git a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
index 1482e87b434d9c3b0567abedd3464113b9cda5b2..6e383786619039f650fe1d79033e5356f801246b 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
@@ -1,28 +1,20 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning:
- Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:81: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:154: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:176: Warning:
+[wp] tests/wp/wp_behav.c:82: Warning:
Missing assigns clause (assigns 'everything' instead)
------------------------------------------------------------
Function assert_needed
------------------------------------------------------------
-Goal Assertion 'ko' (file tests/wp/wp_behav.c, line 117):
+Goal Assertion 'ko' (file tests/wp/wp_behav.c, line 59):
Assume { Type: is_sint32(x). }
Prove: 0 < x.
------------------------------------------------------------
-Goal Assertion 'qed_ok,ok_with_hyp' (file tests/wp/wp_behav.c, line 120):
+Goal Assertion 'qed_ok,ok_with_hyp' (file tests/wp/wp_behav.c, line 62):
Prove: true.
------------------------------------------------------------
@@ -113,19 +105,6 @@ Prove: false.
Goal Assertion for 'x2' 'qed_ok' (file tests/wp/wp_behav.c, line 24):
Prove: true.
-------------------------------------------------------------
-------------------------------------------------------------
- Function local_named_behavior with behavior xpos_stmt_53
-------------------------------------------------------------
-
-Goal Post-condition for 'xpos' 'qed_ok' at instruction (file tests/wp/wp_behav.c, line 112):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition for 'xpos' 'qed_ok' at instruction (file tests/wp/wp_behav.c, line 112):
-Prove: true.
-
------------------------------------------------------------
------------------------------------------------------------
Function min
@@ -175,51 +154,12 @@ Assume {
}
Prove: false.
-------------------------------------------------------------
-------------------------------------------------------------
- Function more_stmt_assigns
-------------------------------------------------------------
-
-Goal Post-condition 'qed_ok,ok_with_hoare' in 'more_stmt_assigns':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function more_stmt_assigns with behavior blk_stmt_86
-------------------------------------------------------------
-
-Goal Assigns for 'blk' 'qed_ok,qed_ok' at block (1/2):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns for 'blk' 'qed_ok,qed_ok' at block (2/2):
-Effect at line 163
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function part_stmt_bhv with behavior b1
-------------------------------------------------------------
-
-Goal Post-condition for 'b1' 'qed_ok' in 'part_stmt_bhv':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function part_stmt_bhv with behavior bs_stmt_93_b1
-------------------------------------------------------------
-
-Goal Post-condition for 'bs' (file tests/wp/wp_behav.c, line 175) at block:
-Assume { Type: is_sint32(x). (* Residual *) When: x <= 0. }
-Prove: false.
-
------------------------------------------------------------
------------------------------------------------------------
Function razT
------------------------------------------------------------
-Goal Preservation of Invariant 'qed_ok' (file tests/wp/wp_behav.c, line 153):
+Goal Preservation of Invariant 'qed_ok' (file tests/wp/wp_behav.c, line 81):
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(n_1).
(* Goal *)
@@ -235,7 +175,7 @@ Prove: T[i <- 0][i_1] = 0.
------------------------------------------------------------
-Goal Establishment of Invariant 'qed_ok' (file tests/wp/wp_behav.c, line 153):
+Goal Establishment of Invariant 'qed_ok' (file tests/wp/wp_behav.c, line 81):
Prove: true.
------------------------------------------------------------
@@ -259,130 +199,3 @@ Assume {
Prove: x = 0.
------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_assigns
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp/wp_behav.c, line 134) in 'stmt_assigns':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_assigns with behavior default_for_stmt_70
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp/wp_behav.c, line 139) at call 'unknown' (file tests/wp/wp_behav.c, line 140):
-Call Effect at line 140
-Prove: false.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract with behavior default_for_stmt_22
-------------------------------------------------------------
-
-Goal Pre-condition 'qed_ok' at block:
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'qed_ok' at block:
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract with behavior ko
-------------------------------------------------------------
-
-Goal Post-condition for 'ko' 'qed_ko' in 'stmt_contract':
-Assume {
- Type: is_sint32(stmt_contract_0).
- (* Post-condition 'qed_ok' at block *)
- Have: 0 < stmt_contract_0.
-}
-Prove: 3 <= stmt_contract_0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract with behavior ko_without_asgn
-------------------------------------------------------------
-
-Goal Post-condition for 'ko_without_asgn' 'qed_ko' in 'stmt_contract':
-Assume {
- Type: is_sint32(Y) /\ is_sint32(stmt_contract_0).
- (* Post-condition 'qed_ok' at block *)
- Have: 0 < stmt_contract_0.
-}
-Prove: Y < stmt_contract_0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract with behavior ok
-------------------------------------------------------------
-
-Goal Post-condition for 'ok' 'qed_ok' in 'stmt_contract':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract_assigns with behavior default_for_stmt_43
-------------------------------------------------------------
-
-Goal Pre-condition 'qed_ok' at block:
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'qed_ok' at block:
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns 'qed_ok,asgn_ok' at block:
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract_assigns with behavior ko
-------------------------------------------------------------
-
-Goal Post-condition for 'ko' 'qed_ko' in 'stmt_contract_assigns':
-Assume {
- Type: is_sint32(stmt_contract_assigns_0).
- (* Post-condition 'qed_ok' at block *)
- Have: 0 < stmt_contract_assigns_0.
-}
-Prove: 3 <= stmt_contract_assigns_0.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract_assigns with behavior ok
-------------------------------------------------------------
-
-Goal Post-condition for 'ok' 'qed_ok' in 'stmt_contract_assigns':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract_assigns with behavior ok_asgn
-------------------------------------------------------------
-
-Goal Post-condition for 'ok_asgn' 'qed_ok' in 'stmt_contract_assigns':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract_label
-------------------------------------------------------------
-
-Goal Post-condition 'qed_ok' in 'stmt_contract_label':
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
- Function stmt_contract_label with behavior default_for_stmt_32
-------------------------------------------------------------
-
-Goal Post-condition 'qed_ok' at block:
-Prove: true.
-
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
index faa679c96697f66156e01511131f9dc0cf867911..3a74aa8479f81fbc1ae664eaf1e71435900d9187 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
@@ -1,18 +1,10 @@
# frama-c -wp -wp-timeout 1 [...]
[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning:
- Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning:
+[wp] tests/wp/wp_behav.c:82: Warning:
Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:81: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:154: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp/wp_behav.c:176: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] 38 goals scheduled
+[wp] 19 goals scheduled
[wp] [Qed] Goal typed_f_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_x1_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_f_assert_qed_ok : Valid
@@ -25,48 +17,22 @@
[wp] [Alt-Ergo] Goal typed_bhv_complete_neg_pos : Valid
[wp] [Qed] Goal typed_bhv_pos_ensures_qed_ok : Valid
[wp] [Qed] Goal typed_bhv_neg_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_requires_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_ok_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_label_ensures_qed_ok_2 : Valid
-[wp] [Qed] Goal typed_stmt_contract_assigns_requires_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_assigns_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_assigns_assigns : Valid
-[wp] [Qed] Goal typed_stmt_contract_assigns_ok_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_stmt_contract_assigns_ok_asgn_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_local_named_behavior_xpos_ensures_qed_ok : Valid
-[wp] [Qed] Goal typed_local_named_behavior_xpos_ensures_qed_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_assert_needed_assert_ko : Unsuccess
[wp] [Qed] Goal typed_assert_needed_assert_qed_ok_ok_with_hyp : Valid
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal typed_bts0513_ensures_ko2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_stmt_assigns_assigns : Unsuccess
-[wp] [Qed] Goal typed_stmt_assigns_ensures : Valid
[wp] [Alt-Ergo] Goal typed_razT_loop_invariant_qed_ok_preserved : Valid
[wp] [Qed] Goal typed_razT_loop_invariant_qed_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_razT_b1_ensures_e1 : Unsuccess
-[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part1 : Valid
-[wp] [Qed] Goal typed_more_stmt_assigns_blk_assigns_part2 : Valid
-[wp] [Qed] Goal typed_more_stmt_assigns_ensures_qed_ok_ok_with_hoare : Valid
-[wp] [Alt-Ergo] Goal typed_part_stmt_bhv_bs_ensures : Unsuccess
-[wp] [Qed] Goal typed_part_stmt_bhv_b1_ensures_qed_ok : Valid
-[wp] Proved goals: 32 / 38
- Qed: 30
- Alt-Ergo: 2 (unsuccess: 6)
+[wp] Proved goals: 15 / 19
+ Qed: 13
+ Alt-Ergo: 2 (unsuccess: 4)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f 5 - 5 100%
min 4 - 4 100%
bhv 2 1 3 100%
- stmt_contract 3 - 3 100%
- stmt_contract_label 2 - 2 100%
- stmt_contract_assigns 5 - 5 100%
- local_named_behavior 2 - 2 100%
assert_needed 1 - 2 50.0%
bts0513 - - 2 0.0%
- stmt_assigns 1 - 2 50.0%
razT 1 1 3 66.7%
- more_stmt_assigns 3 - 3 100%
- part_stmt_bhv 1 - 2 50.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
index 5d374947a3c5b1bd0c93ca6bebb380b8d10df724..96f2e570799cc06bc40f38809d1252960b9b6b3e 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
@@ -1,26 +1,17 @@
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
[wp] Running WP plugin...
-[wp] tests/wp/wp_behav.c:172: Warning:
- Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
-[wp] tests/wp/wp_behav.c:69: Warning:
- Missing assigns clause (assigns 'everything' instead)
-[wp] 8 goals scheduled
+[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_x1_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_f_x2_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_min_bx_ensures_qed_ko : Unsuccess
[wp] [Alt-Ergo] Goal typed_min_by_ensures_qed_ko : Unsuccess
-[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_ensures_qed_ko : Unsuccess
-[wp] [Alt-Ergo] Goal typed_stmt_contract_ko_without_asgn_ensures_qed_ko : Unsuccess
-[wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess
-[wp] Proved goals: 0 / 8
- Alt-Ergo: 0 (unsuccess: 8)
+[wp] Proved goals: 0 / 5
+ Alt-Ergo: 0 (unsuccess: 5)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
f - - 3 0.0%
min - - 2 0.0%
- stmt_contract - - 2 0.0%
- stmt_contract_assigns - - 1 0.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp/wp_behav.c b/src/plugins/wp/tests/wp/wp_behav.c
index 6c4a0817a643305bd4085888967f286fb2add99c..d7b2326cec400765a45ec2f0170e01631d6095a5 100644
--- a/src/plugins/wp/tests/wp/wp_behav.c
+++ b/src/plugins/wp/tests/wp/wp_behav.c
@@ -55,71 +55,13 @@ int bhv (int x, int n) {
return x/n;
}
-/*@ behavior ok: ensures qed_ok: \result > 0;
- behavior ko: ensures qed_ko: \result > 2;
- behavior ko_without_asgn: ensures qed_ko: \result > Y;
-*/
-int stmt_contract (int c) {
- int x = 0;
- Y = 0;
-
- /*@ requires qed_ok: x == 0;
- @ ensures qed_ok: x > 0;
- */
- if (c)
- x = 3;
- else
- x = 5;
- return x;
-}
-
-//@ ensures qed_ok: \result >= 0;
-int stmt_contract_label (int c) {
- int x = 0;
-
- //@ ensures qed_ok: x >= \old(x);
- if (c) x++;
-
- return x;
-}
-
-/*@ behavior ok: ensures qed_ok: \result > 0;
- behavior ko: ensures qed_ko: \result > 2;
- behavior ok_asgn: ensures qed_ok: \result > Y;
-*/
-int stmt_contract_assigns (int c) {
- int x = 0;
- Y = 0;
-
- /*@ requires qed_ok: x == 0;
- @ ensures qed_ok: x > 0;
- @ assigns qed_ok: asgn_ok: x;
- */
- if (c)
- x = 3;
- else
- x = 5;
- return x;
-}
-
-int local_named_behavior (int x) {
- int y = 3;
- /*@ behavior xpos:
- assumes x > 0;
- ensures qed_ok: x > 3;
- ensures qed_ok: x > y;
- */
- x += y;
- return x;
-}
-
void assert_needed (int x) {
//@ assert ko: x > 0;
int a = 0;
a += x;
//@ assert qed_ok: ok_with_hyp: a > 0;
}
-
+
/* we shouldn't be able to prove ko1 from ko2 and then ko2 from ko1 */
/*@ ensures ko1: \result == x+1;
ensures ko2: \result == x+1;
@@ -128,20 +70,6 @@ int bts0513 (int x) {
return x;
}
-//@ assigns X, Y;
-void unknown (int, int);
-
-//@ ensures \result > X;
-int stmt_assigns (int a) {
- int x = 0;
- int y = 3;
- X = x;
- //@ assigns Y;
- unknown (x, y);
- x = x+1;
- return x;
-}
-
int T[10];
// use Inv as Hyp for Bhp props
@@ -151,32 +79,8 @@ int T[10];
void razT (int n) {
//@ loop invariant qed_ok: \forall int k; 0<= k < i ==> T[k] == 0;
- for (int i = 0; i < n; i++)
+ for (int i = 0; i < n; i++)
T[i] = 0;
}
-//@ ensures qed_ok: ok_with_hoare: T[1] == \old(T[1]);
-int more_stmt_assigns (int x) {
- x = 0;
- //@ behavior blk: assigns qed_ok:x, qed_ok:T[x];
- {
- T[x] = 1;
- x = 1;
- }
- return x;
-}
-/*@ behavior b1:
- assumes x > 0;
- ensures qed_ok: \result > x;
-*/
-int part_stmt_bhv (int x) {
- /*@ //TODO: not implemented yet.
- for b1: behavior bs:
- ensures x > \old(x); */
- if (x > 0)
- x++;
- return x;
-}
-
//==============================================================================
-