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