sig
val unreachable_proved : int Stdlib.ref
val unreachable_failed : int Stdlib.ref
val set_unreachable : WpPropId.prop_id -> unit
type asked_assigns = NoAssigns | OnlyAssigns | WithAssigns
val get_call_pre_strategies :
model:WpContext.model -> Cil_types.stmt -> WpStrategy.strategy list
val get_function_strategies :
model:WpContext.model ->
?assigns:WpAnnot.asked_assigns ->
?bhv:string list ->
?prop:string list -> Kernel_function.t -> WpStrategy.strategy list
val get_property_strategies :
model:WpContext.model -> Property.t -> WpStrategy.strategy list
end