module WpAnnot:sig
..end
Properties for assigns of kf
val split : (WpPropId.prop_id -> 'a -> unit) -> WpPropId.prop_id -> 'a Bag.t -> unit
type
proof
val create_proof : WpPropId.prop_id -> proof
val add_proof : proof -> WpPropId.prop_id -> Property.t list -> unit
val is_composed : proof -> bool
val is_proved : proof -> bool
val target : proof -> Property.t
val dependencies : proof -> Property.t list
val filter_status : WpPropId.prop_id -> bool
val get_called_preconditions_at : Cil_types.kernel_function -> Cil_types.stmt -> Property.t list
val get_called_post_conditions : Cil_types.kernel_function -> Property.t list
val get_called_exit_conditions : Cil_types.kernel_function -> Property.t list
val get_called_assigns : Cil_types.kernel_function -> Property.t list
type
asked_assigns =
| |
NoAssigns |
| |
OnlyAssigns |
| |
WithAssigns |
val get_id_prop_strategies : model:Model.t ->
?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list
val get_call_pre_strategies : model:Model.t -> Cil_types.stmt -> WpStrategy.strategy list
val get_function_strategies : model:Model.t ->
?assigns:asked_assigns ->
?bhv:string list ->
?prop:string list -> Kernel_function.t -> WpStrategy.strategy list