diff --git a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
index 33aa35edcaf07f415e355c654d769fd5def32325..032fbb6e3389ad444d994cf762bb34297aeaa5ce 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
@@ -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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
index 3784625aee26490c0486afe4b8f2bdd8b776baa6..1b83f3171c63b1f17daa27356843a9e96ce9c9aa 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
@@ -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%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/terminates_formulae.i b/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
index d0da6ac4cf174372ad88bc3e0342853c1c963f25..cbad957517a53a40dbc52b5c7f1d4c5a8933c627 100644
--- a/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
+++ b/src/plugins/wp/tests/wp_acsl/terminates_formulae.i
@@ -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 ;