[wp] Fixes filter props

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)
 

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 *)