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

wether all partial proofs have been accumulated or not

val target : proof -> Property.t

val dependencies : proof -> Property.t list

val missing_rte : Cil_types.kernel_function -> string 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 : ?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list

val get_call_pre_strategies : Cil_types.stmt -> WpStrategy.strategy list

val get_function_strategies : ?assigns:asked_assigns ->
       ?bhv:string list ->
       ?prop:string list -> Kernel_function.t -> WpStrategy.strategy list