Skip to content
Snippets Groups Projects
Commit bb58530a authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[wp] don't put check-only loop invariants in hypotheses

parent 147c0a38
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/wpAnnot.ml
+ 10
− 5
View file @ bb58530a
......@@ -833,6 +833,8 @@ let add_variant_annot config s ca var_exp loop_entry loop_back =
in loop_entry, loop_back
let add_loop_invariant_annot config vloop s ca b_list inv acc =
let only_check = inv.tp_only_check in
let inv = inv.tp_statement in
let assigns, loop_entry, loop_back , loop_core = acc in
(* we have to prove that inv is true for each edge that goes
* in the loop, so we can assume that inv is true for each edge
......@@ -846,15 +848,18 @@ let add_loop_invariant_annot config vloop s ca b_list inv acc =
WpStrategy.Agoal s ca inv in
let loop_back = add_prop_loop_inv ~established:false config loop_back
WpStrategy.Agoal s ca inv in
let loop_core = add_prop_inv_fixpoint config loop_core
WpStrategy.Ahyp s ca inv in
let loop_core =
if only_check then loop_core
else
add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
in
assigns, loop_entry , loop_back , loop_core
end
| TBRhyp ->
| TBRhyp when not only_check ->
let kind = WpStrategy.Ahyp in
let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
in assigns, loop_entry , loop_back , loop_core
| TBRno -> acc
| TBRhyp | TBRno -> acc
(** Returns the annotations for the three edges of the loop node:
* - loop_entry : goals for the edge entering in the loop
......@@ -865,7 +870,7 @@ let get_loop_annots config vloop s =
let do_annot _ a (assigns, loop_entry, loop_back , loop_core as acc) =
match a.annot_content with
| AInvariant (b_list, true, inv) ->
add_loop_invariant_annot config vloop s a b_list inv.tp_statement acc
add_loop_invariant_annot config vloop s a b_list inv acc
| AVariant (var_exp, None) ->
let loop_entry, loop_back =
add_variant_annot config s a var_exp loop_entry loop_back
......
tests/spec/generalized_check.i
+ 2
− 1
View file @ bb58530a
......@@ -28,10 +28,11 @@ int main() {
void loop () {
int j = 0;
/*@ check loop invariant j == 10;
/*@ check loop invariant false_but_preserved: j == 10;
loop assigns i;
*/
for (int i = 0; i< 10; i++);
/*@ check implied_by_false_invariant: j == 10; */
l: /*@ check invariant \true; */ ;
if (j >= 10) goto l1;
j++;
......
tests/spec/oracle/generalized_check.0.res.oracle
+ 21
− 17
View file @ bb58530a
......@@ -5,24 +5,25 @@
[wp:strategy] take f_assigns *x;
[wp:strategy] [add_node_annots] on <stmt-1>
[wp:strategy] [add_node_annots] on <stmt-2>
[wp:strategy] [add_node_annots] on <stmt-37>
[wp:strategy] [add_node_annots] on <stmt-38>
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] [add_node_annots] on <stmt-17>
[wp:strategy] [add_node_annots] on <stmt-19>
[wp:strategy] [add_node_annots] on <testIn-22>
[wp:strategy] [add_node_annots] on <stmt-23>
[wp:strategy] [add_node_annots] on <stmt-25>
[wp:strategy] [add_node_annots] on <stmt-26>
[wp] tests/spec/generalized_check.i:29: Warning:
Unsupported generalized invariant, use loop invariant instead.
Ignored invariant
check invariant \true;
[wp:strategy] [add_node_annots] on <stmt-26>
[wp:strategy] [add_node_annots] on <testIn-29>
[wp:strategy] [add_node_annots] on <stmt-30>
[wp:strategy] [add_node_annots] on <stmt-32>
[wp:strategy] [add_node_annots] on <stmt-27>
[wp:strategy] [add_node_annots] on <testIn-30>
[wp:strategy] [add_node_annots] on <stmt-31>
[wp:strategy] [add_node_annots] on <stmt-33>
[wp:strategy] [add_node_annots] on <stmt-34>
[wp:strategy] [add_node_annots] on <stmt-41>
[wp:strategy] [add_node_annots] on <stmt-35>
[wp:strategy] [add_node_annots] on <stmt-42>
[wp:strategy] [add_loop_annots] on <loop-20>
[wp:strategy] [add_loop_annots] 1 edges_to_head
[wp:strategy] [add_loop_annots] 2 edges_to_loop
......@@ -39,14 +40,14 @@
[wp:strategy] [add_loop_annots on entry_edges ok]
[wp:strategy] [add_loop_annots on back_edges ok]
[wp:strategy] [add_loop_annots on edges_to_head ok]
[wp:strategy] [add_loop_annots] on <loop-26>
[wp:strategy] [add_loop_annots] on <loop-27>
[wp:strategy] [add_loop_annots] 1 edges_to_head
[wp:strategy] [add_loop_annots] 2 edges_to_loop
[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges
[wp:strategy] [add_loop_annots on entry_edges ok]
[wp:strategy] [add_loop_annots on back_edges ok]
[wp:strategy] [add_loop_annots on edges_to_head ok]
[wp:strategy] [add_loop_annots] on <loop-26>
[wp:strategy] [add_loop_annots] on <loop-27>
[wp:strategy] [add_loop_annots] 1 edges_to_head
[wp:strategy] [add_loop_annots] 2 edges_to_loop
[wp:strategy] [add_loop_annots] 1 back_edges + 1 entry_edges
......@@ -67,7 +68,7 @@
[wp:strategy] [add_node_annots] on <callIn-14>
[wp:strategy] [add_node_annots] on <callIn-14>
[wp:strategy] [add_node_annots] on <stmt-15>
[wp:strategy] [add_node_annots] on <stmt-39>
[wp:strategy] [add_node_annots] on <stmt-40>
[wp] Warning: Missing RTE guards
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
......@@ -120,7 +121,7 @@
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp] tests/spec/generalized_check.i:35: Warning:
[wp] tests/spec/generalized_check.i:36: Warning:
Missing assigns clause (assigns 'everything' instead)
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
......@@ -165,6 +166,7 @@
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
......@@ -250,19 +252,20 @@
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp:strategy] 'main' is the main entry point
[wp] 10 goals scheduled
[wp] 11 goals scheduled
[wp] [Qed] Goal typed_f_assigns : Valid
[wp] [Failed] Goal typed_f_check_f_valid_ko
[wp] [Qed] Goal typed_f_ensures_f_init_x : Valid
[wp] [Failed] Goal typed_lemma_easy_proof
[wp] [Failed] Goal typed_main_check_main_valid_ko
[wp] [Qed] Goal typed_loop_loop_assigns : Valid
[wp] [Failed] Goal typed_loop_loop_invariant_established
[wp] [Qed] Goal typed_loop_loop_invariant_preserved : Valid
[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
[wp] [Failed] Goal typed_loop_loop_invariant_false_but_preserved_established
[wp] [Failed] Goal typed_loop_loop_invariant_false_but_preserved_preserved
[wp] [Failed] Goal typed_main_call_f_requires_f_valid_x
[wp] [Failed] Goal typed_main_check_main_p_content_ko
[wp] Proved goals: 4 / 10
Qed: 4
[wp] [Failed] Goal typed_main_check_main_valid_ko
[wp] Proved goals: 3 / 11
Qed: 3
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'f' is NOT the main entry point
[wp:strategy] 'loop' is NOT the main entry point
......@@ -309,10 +312,11 @@ void loop(void)
int j = 0;
{
int i = 0;
/*@ check loop invariant j ≡ 10;
/*@ check loop invariant false_but_preserved: j ≡ 10;
loop assigns i; */
while (i < 10) i ++;
}
/*@ check implied_by_false_invariant: j ≡ 10; */ ;
l: /*@ check invariant \true; */ ;
if (j >= 10) goto l1;
j ++;
......
tests/spec/oracle/generalized_check.1.res.oracle
+ 5
− 3
View file @ bb58530a
......@@ -16,8 +16,10 @@
[eva:alarm] tests/spec/generalized_check.i:25: Warning:
check 'main_p_content_ko' got status unknown.
[eva:alarm] tests/spec/generalized_check.i:31: Warning:
loop invariant got status invalid.
loop invariant 'false_but_preserved' got status invalid.
[eva] tests/spec/generalized_check.i:34: starting to merge loop iterations
[eva:alarm] tests/spec/generalized_check.i:35: Warning:
check 'implied_by_false_invariant' got status invalid.
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function loop:
......@@ -29,7 +31,7 @@
[eva:summary] ====== ANALYSIS SUMMARY ======
----------------------------------------------------------------------------
3 functions analyzed (out of 3): 100% coverage.
In these functions, 24 statements reached (out of 27): 88% coverage.
In these functions, 25 statements reached (out of 28): 89% coverage.
----------------------------------------------------------------------------
Some errors and warnings have been raised during the analysis:
by the Eva analyzer: 0 errors 1 warning
......@@ -39,7 +41,7 @@
1 access to uninitialized left-values
----------------------------------------------------------------------------
Evaluation of the logical properties reached by the analysis:
Assertions 0 valid 2 unknown 1 invalid 3 total
Assertions 0 valid 2 unknown 2 invalid 4 total
Preconditions 0 valid 1 unknown 0 invalid 1 total
0% of the logical properties reached have been proven.
----------------------------------------------------------------------------
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