From bb1bc134f4ea99e54d5b89f970b6d0e010aa54aa Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 8 Feb 2021 13:50:04 +0100
Subject: [PATCH] [wp] Fixes filter props

---
 src/plugins/wp/cfgInfos.ml  | 10 ++++++++--
 src/plugins/wp/wpPropId.mli |  3 +++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index b679aebcbff..382b516da8f 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -92,7 +92,13 @@ let selected_name ~prop name =
 
 let selected_assigns ~prop = function
   | Cil_types.WritesAny -> false
-  | _ -> selected_name ~prop "@assigns"
+  | Writes _ when prop = [] -> true
+  | Writes l ->
+    let collect_names l (t, _) =
+      WpPropId.ident_names t.Cil_types.it_content.term_name @ l
+    in
+    let names = List.fold_left collect_names ["@assigns"] l in
+    WpPropId.are_selected_names prop names
 
 let selected_allocates ~prop = function
   | Cil_types.FreeAllocAny -> false
@@ -100,7 +106,7 @@ let selected_allocates ~prop = function
 
 let selected_precond ~prop ip =
   prop = [] ||
-  let tk_name = "@ensures" in
+  let tk_name = "@requires" in
   let tp_names = WpPropId.user_pred_names ip.Cil_types.ip_content in
   WpPropId.are_selected_names prop (tk_name :: tp_names)
 
diff --git a/src/plugins/wp/wpPropId.mli b/src/plugins/wp/wpPropId.mli
index 45d5c451922..d98e533eea1 100644
--- a/src/plugins/wp/wpPropId.mli
+++ b/src/plugins/wp/wpPropId.mli
@@ -71,6 +71,9 @@ val select_for_behaviors : string list -> prop_id -> bool
 (** test if the prop_id has to be selected when we want to select the call. *)
 val select_call_pre : stmt -> Property.t option -> prop_id -> bool
 
+(** From a list of names (of an identified terms), returns usable names. *)
+val ident_names : string list -> string list
+
 (*----------------------------------------------------------------------------*)
 
 val prop_id_keys : prop_id -> string list * string list (* required , hints *)
-- 
GitLab