Module WpAnnot

module WpAnnot: sig .. end

Every access to annotations have to go through here, so this is the place where we decide what the computation is allowed to use.

val unreachable_proved : int Stdlib.ref
val unreachable_failed : int Stdlib.ref
val trivial_terminates : int Stdlib.ref
val set_unreachable : WpPropId.prop_id -> unit
val set_trivially_terminates : WpPropId.prop_id -> Property.Set.t -> 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: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