Commit 02823c97 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] WpTarget takes fors in account

parent 0224bc4f
......@@ -78,12 +78,11 @@ exception Found
let check_properties behaviors props kf =
let open Property in
let selected_behavior b =
behaviors = [] ||
Extlib.may_map ~dft:false (fun b -> List.mem b.b_name behaviors) b
let exists_selected_behavior l =
behaviors = [] || List.exists (fun b -> List.mem b behaviors) l
in
let check_ip ip =
if selected_behavior (get_behavior ip) then
if exists_selected_behavior (WpPropId.user_bhv_names ip) then
let names = WpPropId.user_prop_names ip in
if props = [] || WpPropId.are_selected_names props names then raise Found
in
......
......@@ -521,6 +521,22 @@ let user_prop_names p =
| IPGlobalInvariant _
| IPOther _ -> []
let user_bhv_names p =
let open Property in
let fors = match p with
| Property.IPCodeAnnot { ica_ca } ->
let fors = match ica_ca.annot_content with
| Cil_types.AAssert (fors, _)
| Cil_types.AStmtSpec (fors, _)
| Cil_types.AInvariant (fors, _, _)
| Cil_types.AAssigns (fors, _)
| Cil_types.AAllocation (fors, _)
| Cil_types.AExtended (fors, _, _) -> fors
| _ -> []
in fors
| _ -> []
in Extlib.may_map ~dft:fors (fun b -> b.b_name :: fors) (get_behavior p)
let string_of_termination_kind = function
Normal -> "post"
| Exits -> "exits"
......
......@@ -80,6 +80,7 @@ val get_propid : prop_id -> string (** Unique identifier of [prop_id] *)
val get_legacy : prop_id -> string (** Unique legacy identifier of [prop_id] *)
val pp_propid : Format.formatter -> prop_id -> unit (** Print unique id of [prop_id] *)
val user_bhv_names: Property.identified_property -> string list
val user_prop_names: Property.identified_property -> string list
val are_selected_names: string list -> string list -> bool
(** [are_selected_names asked names] checks if [names] of a property are
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment