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