Skip to content
Snippets Groups Projects
Commit 3150f058 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] fix precondition filtering

parent 562a23a5
No related branches found
No related tags found
No related merge requests found
......@@ -85,8 +85,7 @@ let is_active_mode ~mode ~goal (p: Property.t) =
| IPCodeAnnot { ica_ca } -> is_selected_ca mode ~goal ica_ca
| IPPredicate { ip_kind } ->
begin match ip_kind with
| PKRequires bhv | PKAssumes bhv ->
Cil.is_default_behavior bhv || is_selected_bhv mode bhv
| PKRequires _ | PKAssumes _ -> true
| PKEnsures(bhv,_) -> is_selected_bhv mode bhv
| PKTerminates -> is_default_bhv mode
end
......
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