sig
val split :
(WpPropId.prop_id -> 'a -> unit) -> WpPropId.prop_id -> 'a Bag.t -> unit
type proof
val create_proof : WpPropId.prop_id -> WpAnnot.proof
val add_proof :
WpAnnot.proof -> WpPropId.prop_id -> Property.t list -> unit
val is_composed : WpAnnot.proof -> bool
val is_proved : WpAnnot.proof -> bool
val target : WpAnnot.proof -> Property.t
val dependencies : WpAnnot.proof -> Property.t list
val missing_rte : Cil_types.kernel_function -> string 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 :
?assigns:WpAnnot.asked_assigns -> Property.t -> WpStrategy.strategy list
val get_call_pre_strategies : Cil_types.stmt -> WpStrategy.strategy list
val get_function_strategies :
?assigns:WpAnnot.asked_assigns ->
?bhv:string list ->
?prop:string list -> Kernel_function.t -> WpStrategy.strategy list
end