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.

Properties for assigns of kf


type proof 
A proof accumulator for a set of related prop_id
val create_proof : WpPropId.prop_id -> proof
to be used only once for one of the related prop_id
val add_proof : proof -> WpPropId.prop_id -> Property.t list -> unit
accumulate in the proof the partial proof for this prop_id
val add_invalid_proof : proof -> unit
add an invalid proof result ; can not revert a complete proof
val is_composed : proof -> bool
whether a proof needs several lemma to be complete
val is_proved : proof -> bool
whether all partial proofs have been accumulated or not
val is_invalid : proof -> bool
whether an invalid proof result has been registered or not
val status : proof -> [ `Invalid | `Partial | `Proved ]
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
Properties for assigns of kf
type asked_assigns = 
| NoAssigns
| OnlyAssigns
| WithAssigns
val get_id_prop_strategies : model:WpContext.model ->
?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list
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