Skip to content
Snippets Groups Projects
Commit cada6a33 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Test terminates formulae checks call labels

parent 8eeaed5d
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/terminates_formulae.res.oracle
+ 79
− 14
View file @ cada6a33
......@@ -3,36 +3,101 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call
Function base_call
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 20) in 'call' (1/2):
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 22) in 'base_call' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 20) in 'call' (2/2):
Call Effect at line 22
Assume { (* Goal *) When: P_Q. }
Prove: P_P.
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 22) in 'base_call' (2/2):
Call Effect at line 24
Assume { (* Heap *) Type: is_sint32(a). (* Goal *) When: P_Q. }
Prove: P_P(a).
------------------------------------------------------------
------------------------------------------------------------
Function call_change
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 32) in 'call_change' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 32) in 'call_change' (2/2):
Call Effect at line 35
Assume { (* Heap *) Type: is_sint32(a). (* Goal *) When: P_P(a). }
Prove: P_P(0).
------------------------------------------------------------
------------------------------------------------------------
Function call_param_change
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 48) in 'call_param_change' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 48) in 'call_param_change' (2/2):
Call Effect at line 51
Let x = Mint_0[p].
Assume {
Type: is_sint32(x).
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
When: x != 0.
}
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function call_param_same
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 43) in 'call_param_same' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 43) in 'call_param_same' (2/2):
Call Effect at line 45
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function call_same
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 27) in 'call_same' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 27) in 'call_same' (2/2):
Call Effect at line 29
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function no_variant
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 33) in 'no_variant' (1/2):
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 62) in 'no_variant' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 33) in 'no_variant' (2/2):
Effect at line 36
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 62) in 'no_variant' (2/2):
Effect at line 65
Prove: !P_Q.
------------------------------------------------------------
Goal Loop assigns (file tests/wp_acsl/terminates_formulae.i, line 35):
Goal Loop assigns (file tests/wp_acsl/terminates_formulae.i, line 64):
Prove: true.
------------------------------------------------------------
......@@ -40,23 +105,23 @@ Prove: true.
Function variant
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 25) in 'variant':
Goal Termination-condition (file tests/wp_acsl/terminates_formulae.i, line 54) in 'variant':
Prove: true.
------------------------------------------------------------
Goal Loop assigns (file tests/wp_acsl/terminates_formulae.i, line 27):
Goal Loop assigns (file tests/wp_acsl/terminates_formulae.i, line 56):
Prove: true.
------------------------------------------------------------
Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_formulae.i, line 30):
Goal Decreasing of Loop variant at loop (file tests/wp_acsl/terminates_formulae.i, line 59):
Assume { Type: is_uint32(i). (* Goal *) When: P_Q. (* Then *) Have: 0 < i. }
Prove: to_uint32(i - 1) < i.
------------------------------------------------------------
Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_formulae.i, line 30):
Goal Positivity of Loop variant at loop (file tests/wp_acsl/terminates_formulae.i, line 59):
Prove: true.
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+ 19
− 7
View file @ cada6a33
......@@ -2,9 +2,17 @@
[kernel] Parsing tests/wp_acsl/terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_call_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_call_terminates_part2 : Unsuccess
[wp] 17 goals scheduled
[wp] [Qed] Goal typed_base_call_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_base_call_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_call_same_terminates_part1 : Valid
[wp] [Qed] Goal typed_call_same_terminates_part2 : Valid
[wp] [Qed] Goal typed_call_change_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_call_change_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_call_param_same_terminates_part1 : Valid
[wp] [Qed] Goal typed_call_param_same_terminates_part2 : Valid
[wp] [Qed] Goal typed_call_param_change_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_call_param_change_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_variant_terminates : Valid
[wp] [Qed] Goal typed_variant_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_variant_loop_variant_decrease : Valid
......@@ -12,12 +20,16 @@
[wp] [Qed] Goal typed_no_variant_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_no_variant_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_no_variant_loop_assigns : Valid
[wp] Proved goals: 7 / 9
Qed: 6
Alt-Ergo: 1 (unsuccess: 2)
[wp] Proved goals: 13 / 17
Qed: 12
Alt-Ergo: 1 (unsuccess: 4)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
call 1 - 2 50.0%
base_call 1 - 2 50.0%
call_same 2 - 2 100%
call_change 1 - 2 50.0%
call_param_same 2 - 2 100%
call_param_change 1 - 2 50.0%
variant 3 1 4 100%
no_variant 2 - 3 66.7%
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/terminates_formulae.i
+ 31
− 2
View file @ cada6a33
......@@ -5,9 +5,11 @@
OPT: -wp-variant-with-terminates
*/
int a ;
/*@
axiomatic Ax {
predicate P reads \nothing ;
predicate P reads a ;
predicate Q reads \nothing ;
}
*/
......@@ -18,10 +20,37 @@
void terminates_P(void);
//@ terminates Q ;
void call(void){
void base_call(void){
terminates_P();
}
//@ terminates P ;
void call_same(void){
terminates_P();
}
//@ terminates P ;
void call_change(void){
a = 0 ;
terminates_P();
}
/*@ terminates *p ;
assigns \nothing ;
*/
void call_param(int* p);
//@ terminates *p ;
void call_param_same(int *p){
call_param(p);
}
//@ terminates *p ;
void call_param_change(int *p){
*p = 0 ;
call_param(p);
}
//@ terminates Q ;
void variant(void){
/*@ loop assigns i ;
......
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