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

[wp] ignore check loop when searching for dead annot

parent da629511
No related branches found
No related tags found
No related merge requests found
......@@ -84,9 +84,9 @@ let is_dead_annot ca =
match ca.annot_content with
| APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
false && is_unrolled_completely spec
| AAssert([],p) ->
| AAssert([],p)
| AInvariant([],_,p) ->
not p.tp_only_check && is_predicate false p.tp_statement
| AInvariant([],_,p) -> is_predicate false p.tp_statement
| _ -> false
let is_dead_code stmt =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment