From 3150f058a4d5bab265c419fa35e2a0edee832304 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 15 Feb 2021 16:23:20 +0100
Subject: [PATCH] [wp] fix precondition filtering
---
src/plugins/wp/cfgCalculus.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index ef586c7c564..d886bdacd26 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -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
--
GitLab