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