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.


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 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