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

[wp] fix decreases caller evaluation

parent beceec74
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 82 additions and 20 deletions
src/plugins/wp/cfgAnnot.ml
+ 11
− 4
View file @ 250a5c94
......@@ -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 ;
......
src/plugins/wp/normAtLabels.ml
+ 4
− 0
View file @ 250a5c94
......@@ -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 =
......
src/plugins/wp/normAtLabels.mli
+ 1
− 0
View file @ 250a5c94
......@@ -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
src/plugins/wp/tests/wp_acsl/decreases.i
+ 12
− 0
View file @ 250a5c94
......@@ -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();
}
}
src/plugins/wp/tests/wp_acsl/oracle/decreases.0.res.oracle
+ 14
− 2
View file @ 250a5c94
......@@ -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.
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle/decreases.1.res.oracle
+ 14
− 2
View file @ 250a5c94
......@@ -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.
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle/terminates_formulae.res.oracle
+ 3
− 1
View file @ 250a5c94
......@@ -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)
......
src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.0.res.oracle
+ 10
− 5
View file @ 250a5c94
......@@ -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%
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle_qualif/decreases.1.res.oracle
+ 10
− 5
View file @ 250a5c94
......@@ -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%
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle_qualif/terminates_formulae.res.oracle
+ 3
− 1
View file @ 250a5c94
......@@ -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)
......
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