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


val split : (WpPropId.prop_id -> 'a -> unit) -> WpPropId.prop_id -> 'a Bag.t -> unit
splits a prop_id goals into prop_id parts for each sub-goals
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 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 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: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