diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 425f3df70fe94de264fd1e941535ffcd4c14e45e..9e529fc7c44f60f8bfd71fb04f74271d5573bcc8 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -91,6 +91,12 @@ let normalize_post ~goal kf bhv tk ?assumes (itk,ip) =
Some (id , implies ?assumes p)
else None
+let normalize_decreases (d, li) =
+ let module L = NormAtLabels in
+ let at_pre e = Logic_const.tat (e, BuiltinLabel Pre) in
+ let labels = L.labels_fct_pre in
+ (at_pre @@ L.preproc_term labels d, li)
+
let normalize_froms tk froms =
let module L = NormAtLabels in
let labels = L.labels_fct_assigns ~exit:(tk=Exits) in
@@ -246,12 +252,13 @@ let get_terminates_hyp kf =
let check_variant_relation = function
| (_, None) -> ()
- | (_, Some rel) ->
- Wp_parameters.hypothesis ~once:true
+ | ({ term_loc }, Some rel) ->
+ Wp_parameters.hypothesis
+ ~source:(fst term_loc) ~once:true
"'%a' relation must be well-founded" Cil_printer.pp_logic_info rel
let get_decreases_goal kf =
- let defined t = WpPropId.mk_decrease_id kf Kglobal t, t in
+ let defined t = WpPropId.mk_decrease_id kf Kglobal t, normalize_decreases t in
match Annotations.decreases ~populate:false kf with
| None -> None
| Some v -> check_variant_relation v ; Some (defined v)
@@ -348,7 +355,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| Writes froms -> Writes (normalize_froms Normal froms)
in
let terminates = get_terminates_hyp kf in
- let decreases = get_decreases_hyp kf in
+ let decreases = Option.map normalize_decreases @@ get_decreases_hyp kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
diff --git a/src/plugins/wp/normAtLabels.ml b/src/plugins/wp/normAtLabels.ml
index 0033fe47bf1468749bc80c1fa958a8ebb601297a..4ae48410ed5e5b8e6a7bb8e302698328ab627e62 100644
--- a/src/plugins/wp/normAtLabels.ml
+++ b/src/plugins/wp/normAtLabels.ml
@@ -214,6 +214,10 @@ let preproc_annot labels p =
let visitor = new norm_at labels in
Visitor.visitFramacPredicate visitor p
+let preproc_term labels t =
+ let visitor = new norm_at labels in
+ Visitor.visitFramacTerm visitor t
+
(** @raise LabelError if there is a label in [p] that is incompatible
* with the [labels] translation *)
let preproc_assigns labels asgns =
diff --git a/src/plugins/wp/normAtLabels.mli b/src/plugins/wp/normAtLabels.mli
index dfa2f0962e42c72ebf47b3d4e9453987416a19c4..73e5c5ca0be2074e063955cf51a19497f891895f 100644
--- a/src/plugins/wp/normAtLabels.mli
+++ b/src/plugins/wp/normAtLabels.mli
@@ -42,6 +42,7 @@ val labels_stmt_assigns_l : kf:kernel_function -> stmt -> c_label option -> labe
val labels_predicate : (logic_label * logic_label) list -> label_mapping
val labels_axiom : label_mapping
+val preproc_term : label_mapping -> term -> term
val preproc_annot : label_mapping -> predicate -> predicate
val preproc_assigns : label_mapping -> from list -> from list
val has_postassigns : assigns -> bool
diff --git a/src/plugins/wp/tests/wp_acsl/decreases.i b/src/plugins/wp/tests/wp_acsl/decreases.i
index b4d482fe2e6de2726ac360465942eae7a6a6f128..c264819eb94cff0ae29c3bde85d226946495dea0 100644
--- a/src/plugins/wp/tests/wp_acsl/decreases.i
+++ b/src/plugins/wp/tests/wp_acsl/decreases.i
@@ -111,3 +111,15 @@ void mw2(unsigned x){
(void)fact(x); // no verification of decreases here
}
+
+// Recursion with side-effect
+
+int x ;
+
+//@ decreases x ;
+void se(void){
+ if (x > 0){
+ x -- ;
+ se();
+ }
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
index 1c0241e1df554d73e7532ba44337a17271391de2..d20b06232776956bd66553f5a393316e9f2574d6 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
@@ -2,11 +2,14 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
------------------------------------------------------------
@@ -240,3 +243,12 @@ Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: P_Wrong(x, to_uint32(x - 1)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function se
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 123
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
index 503c417688228f6147615930e14def6d47a18997..acfb72158d91d27f3953083bfe93b24b4d9e0178 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
@@ -2,11 +2,14 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
------------------------------------------------------------
@@ -257,3 +260,12 @@ Assume { Type: is_uint32(x). (* Then *) Have: 11 <= x. }
Prove: P_Wrong(x, to_uint32(x - 1)).
------------------------------------------------------------
+------------------------------------------------------------
+ Function se
+------------------------------------------------------------
+
+Goal Recursion variant:
+Call Effect at line 123
+Prove: true.
+
+------------------------------------------------------------
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 d9bd70618f767ce264637cc140e5ee6199eadd5d..d8eeb1c7538d13ae49466588dcd4070e164b29ba 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
@@ -2,7 +2,9 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:90: Warning:
+[wp:hypothesis] terminates_formulae.i:84: Warning:
+ 'Rel' relation must be well-founded
+[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
index 62e79688690128fd49abbc91e54a2e4c560df53d..a87bf3324219a0f849a14aee28f61793d56182f3 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
@@ -2,14 +2,17 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
-[wp] 26 goals scheduled
+[wp] 27 goals scheduled
[wp] [Qed] Goal typed_fact_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fact_variant : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_variant : Unsuccess
@@ -36,8 +39,9 @@
[wp] [Alt-Ergo] Goal typed_mw2_variant_part1 : Unsuccess (Degenerated)
[wp] [Alt-Ergo] Goal typed_mw2_variant_part2 : Valid
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
-[wp] Proved goals: 17 / 26
- Qed: 6
+[wp] [Qed] Goal typed_se_variant : Valid
+[wp] Proved goals: 18 / 27
+ Qed: 7
Alt-Ergo: 11 (unsuccess: 9)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -54,4 +58,5 @@
mt1 1 1 3 66.7%
mw2 - 1 2 50.0%
mw1 - - 1 0.0%
+ se 1 - 1 100%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
index 63e3fba1f7426ce524df7c0e5c5f319d6f557091..541e824ca018457efbf91c512ea2ac7bd2794e1f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
@@ -2,14 +2,17 @@
[kernel] Parsing decreases.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] decreases.i:108: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:44: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:25: Warning: 'Rel' relation must be well-founded
+[wp:hypothesis] decreases.i:30: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:71: Warning: No decreases clause for missing_2
-[wp:hypothesis] decreases.i:108: Warning: 'Wrong' relation must be well-founded
+[wp:hypothesis] decreases.i:107: Warning: 'Wrong' relation must be well-founded
[wp] decreases.i:109: Warning:
On call to mw1, relation (Wrong) does not match caller (Rel)
+[wp:hypothesis] decreases.i:103: Warning: 'Rel' relation must be well-founded
[wp] decreases.i:105: Warning:
On call to mw2, relation (Rel) does not match caller (Wrong)
-[wp] 26 goals scheduled
+[wp] 27 goals scheduled
[wp] [Qed] Goal typed_fact_terminates : Valid
[wp] [Alt-Ergo] Goal typed_fact_variant : Valid
[wp] [Alt-Ergo] Goal typed_fails_fact_variant : Unsuccess
@@ -36,8 +39,9 @@
[wp] [Alt-Ergo] Goal typed_mw2_variant_part1 : Unsuccess (Degenerated)
[wp] [Alt-Ergo] Goal typed_mw2_variant_part2 : Valid
[wp] [Alt-Ergo] Goal typed_mw1_variant : Unsuccess (Degenerated)
-[wp] Proved goals: 18 / 26
- Qed: 7
+[wp] [Qed] Goal typed_se_variant : Valid
+[wp] Proved goals: 19 / 27
+ Qed: 8
Alt-Ergo: 11 (unsuccess: 8)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
@@ -54,4 +58,5 @@
mt1 1 1 3 66.7%
mw2 - 1 2 50.0%
mw1 - - 1 0.0%
+ se 1 - 1 100%
------------------------------------------------------------
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 cf90d39ba3fc26032ba408a35e80cd1c1badb88a..cb8634fd614c650bd783d59986c144dc533969fa 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,7 +2,9 @@
[kernel] Parsing terminates_formulae.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp:hypothesis] terminates_formulae.i:90: Warning:
+[wp:hypothesis] terminates_formulae.i:84: Warning:
+ 'Rel' relation must be well-founded
+[wp:hypothesis] terminates_formulae.i:67: Warning:
'Rel' relation must be well-founded
[wp] [CFG] Goal general_variant_terminates : Valid (Trivial)
[wp] [CFG] Goal variant_terminates : Valid (Trivial)