module WpAnnot: sig
.. end
Properties for assigns of kf
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 dkey : Log.category
val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
val rte_find : (unit -> 'a * 'b * ('c -> bool)) Pervasives.ref -> 'c -> bool
val rte_precond_status : Kernel_function.t -> bool
val rte_signedOv_status : Cil_types.kernel_function -> bool
val rte_divMod_status : Cil_types.kernel_function -> bool
val _rte_downCast_status : Cil_types.kernel_function -> bool
val rte_memAccess_status : Cil_types.kernel_function -> bool
val rte_unsignedOv_status : Cil_types.kernel_function -> bool
val rte_wp : (string * (Cil_types.kernel_function -> bool) * string) list
val missing_rte : Cil_types.kernel_function -> string list
val compute_rte_for : Cil_types.kernel_function -> unit
val get_called_postconds : Cil_types.termination_kind ->
Cil_types.kernel_function -> Property.identified_property list
val get_called_post_conditions : Cil_types.kernel_function -> Property.identified_property list
val get_called_exit_conditions : Cil_types.kernel_function -> Property.identified_property list
val get_called_assigns : Cil_types.kernel_function -> Property.identified_property list
Properties for assigns of kf
val wp_unreachable : Emitter.t
val set_unreachable : WpPropId.prop_id -> unit
type
proof = {
|
target : Property.t ; |
|
proved : proofpart array ; |
|
mutable dependencies : Property.Set.t ; |
}
A proof accumulator for a set of related prop_id
type
proofpart =
val target : proof -> Property.t
val dependencies : proof -> Property.Set.elt list
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 mk_call_pre_id : Cil_types.kernel_function ->
Cil_types.funbehavior ->
Cil_types.stmt -> Cil_types.identified_predicate -> WpPropId.prop_id
val call_preconditions : Cil_types.kernel_function -> Cil_types.stmt -> (Property.t * Property.t) list
val preconditions_at_call : Cil_types.stmt -> Cil2cfg.call_type -> WpPropId.prop_id list
val get_called_preconditions_at : Cil_types.kernel_function -> Cil_types.stmt -> Property.t list
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
asked_assigns =
| |
NoAssigns |
| |
OnlyAssigns |
| |
WithAssigns |
type
asked_bhv =
val name_of_asked_bhv : asked_bhv -> string
type
asked_prop =
| |
AllProps |
| |
NamedProp of string list |
| |
IdProp of Property.t |
| |
CallPre of Cil_types.stmt * Property.t option |
module HdefAnnotBhv: Cil2cfg.HE
(
sig
end
)
type
strategy_info = {
}
val pp_assigns_mode : Format.formatter -> strategy_info -> unit
val pp_asked_prop : Format.formatter -> strategy_info -> unit
val pp_strategy_info : Format.formatter -> strategy_info -> unit
val cur_fct_default_bhv : strategy_info -> bool
val filter_assign : strategy_info -> WpPropId.prop_id -> bool
val filter_speconly : strategy_info -> WpPropId.prop_id -> bool
val filter_status : WpPropId.prop_id -> bool
val filter_configstatus : strategy_info -> WpPropId.prop_id -> bool
val filter_asked : strategy_info -> WpPropId.prop_id -> bool
val filter : 'a -> 'b -> (('a -> 'b -> bool) * 'c) list -> 'c option
val dkey : Log.category
val goal_to_select : strategy_info -> WpPropId.prop_id -> bool
val kind_to_select : strategy_info ->
WpStrategy.annot_kind -> WpPropId.prop_id -> WpStrategy.annot_kind option
val add_prop_inv_establish : strategy_info ->
WpStrategy.t_annots ->
WpStrategy.annot_kind ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.predicate Cil_types.named -> WpStrategy.t_annots
val add_prop_inv_preserve : strategy_info ->
WpStrategy.t_annots ->
WpStrategy.annot_kind ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.predicate Cil_types.named -> WpStrategy.t_annots
val add_prop_inv_fixpoint : strategy_info ->
WpStrategy.t_annots ->
WpStrategy.annot_kind ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.predicate Cil_types.named -> WpStrategy.t_annots
val add_loop_assigns_goal : strategy_info ->
Cil_types.stmt ->
Cil_types.code_annotation * Cil_types.identified_term Cil_types.from list ->
WpStrategy.t_annots -> WpStrategy.t_annots
val add_stmt_assigns_goal : strategy_info ->
Cil_types.stmt ->
WpStrategy.t_annots ->
Cil_types.funbehavior -> Cil_types.logic_label option -> WpStrategy.t_annots
val add_fct_assigns_goal : strategy_info ->
WpStrategy.t_annots ->
Cil_types.termination_kind -> Cil_types.funbehavior -> WpStrategy.t_annots
val get_named_bhv : string ->
('a, 'b) Cil_types.behavior list -> ('a, 'b) Cil_types.behavior option
find the behavior named name
in the list
val get_behav : strategy_info ->
Cil_types.kinstr ->
('a, 'b) Cil_types.behavior list -> ('a, 'b) Cil_types.behavior option
Select in bhv_list
the behavior that has to be processed
according to config
and ki
current statement.
type
test_behav_res =
| |
TBRno |
| |
TBRhyp |
| |
TBRpart |
| |
TBRok |
Tells weather the property belonging to the behaviors in bhv_name_list
has to be considered according to config
.
val is_annot_for_config : strategy_info ->
Cil2cfg.node -> Cil_types.stmt -> string list -> test_behav_res
(see test_behav_res
above).
If the annotation doesn't have "for" names, it is a bit complicated because
we have to know if the statement s
is inside a stmt behavior or not.
val add_fct_pre : strategy_info ->
WpStrategy.t_annots -> Cil_types.funspec -> WpStrategy.t_annots
val add_variant : 'a -> (Cil_types.term, 'b, 'c) Cil_types.spec -> 'a
val add_terminates : 'a -> ('b, Cil_types.identified_predicate, 'c) Cil_types.spec -> 'a
val add_disjoint_behaviors_props : strategy_info ->
Cil_types.kinstr ->
Cil_types.funspec -> WpStrategy.t_annots -> WpStrategy.t_annots
val add_complete_behaviors_props : strategy_info ->
Cil_types.kinstr ->
Cil_types.funspec -> WpStrategy.t_annots -> WpStrategy.t_annots
val add_behaviors_props : strategy_info ->
Cil_types.kinstr ->
Cil_types.funspec -> WpStrategy.t_annots -> WpStrategy.t_annots
val add_stmt_spec_post_as_hyp : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
Cil_types.funspec ->
WpStrategy.t_annots * WpStrategy.t_annots ->
WpStrategy.t_annots * WpStrategy.t_annots
Add the post condition of the whole spec as hypothesis.
Add old(assumes) => ensures
for all the behaviors,
and also add an upper approximation of the merged assigns information.
val add_stmt_bhv_as_goal : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
Cil_types.funbehavior ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots) ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots)
we want to prove this behavior:
- add the requires as preconditions to both prove and use as hyp,
- add the assumes as hypotheses,
- add the postconditions as goals.
val is_empty_behavior : ('a, 'b) Cil_types.behavior -> bool
val is_empty_spec : ('a, 'b, 'c) Cil_types.spec -> bool
val add_stmt_spec_annots : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
Cil_types.funspec ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots) ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots)
val add_called_pre : strategy_info ->
Cil_types.kernel_function ->
Cil_types.stmt ->
('a, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec -> WpStrategy.t_annots -> WpStrategy.t_annots
val add_called_post : Cil_types.kernel_function ->
Cil_types.termination_kind -> WpStrategy.t_annots -> WpStrategy.t_annots
val add_call_annots : strategy_info ->
Cil_types.stmt ->
Cil_types.kernel_function ->
Cil_types.logic_label option ->
bool ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots) ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots)
val get_call_annots : strategy_info ->
Cil2cfg.node ->
Cil_datatype.Stmt.t ->
Cil2cfg.call_type ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots)
val add_variant_annot : strategy_info ->
Cil_types.stmt ->
Cil_types.code_annotation ->
Cil_types.term -> 'a -> WpStrategy.t_annots -> 'a * WpStrategy.t_annots
val add_loop_invariant_annot : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
Cil_types.code_annotation ->
string list ->
Cil_types.predicate Cil_types.named ->
'a * WpStrategy.t_annots * WpStrategy.t_annots * WpStrategy.t_annots ->
'a * WpStrategy.t_annots * WpStrategy.t_annots * WpStrategy.t_annots
val add_stmt_invariant_annot : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
Cil_types.code_annotation ->
string list ->
Cil_types.predicate Cil_types.named ->
WpStrategy.t_annots * 'a -> WpStrategy.t_annots * 'a
val get_loop_annots : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
WpStrategy.t_annots * WpStrategy.t_annots * WpStrategy.t_annots
Returns the annotations for the three edges of the loop node:
- loop_entry : goals for the edge entering in the loop
- loop_back : goals for the edge looping to the entry point
- loop_core : fix-point hypothesis for the edge starting the loop core
val get_stmt_annots : strategy_info ->
Cil2cfg.node ->
Cil_types.stmt ->
WpStrategy.t_annots * (WpStrategy.t_annots * WpStrategy.t_annots)
val get_fct_pre_annots : strategy_info -> Cil_types.funspec -> WpStrategy.t_annots
val get_fct_post_annots : strategy_info ->
Cil_types.termination_kind ->
('a, Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.spec -> WpStrategy.t_annots
val get_behavior_annots : strategy_info -> WpStrategy.annots_tbl
Builds tables that give hypotheses and goals relative to b
behavior
for edges of the cfg to consider during wp computation.
b = None
means that we only consider internal properties to select for the
default behavior. This is useful when the function doesn't have any
specification.
module GS: Cil_datatype.Global_annotation.Set
val add_global_annotations : WpStrategy.annots_tbl -> WpStrategy.annots_tbl
val behavior_name_of_config : strategy_info -> string option
val build_bhv_strategy : strategy_info -> WpStrategy.strategy
val internal_function_behaviors : Cil2cfg.t ->
(Cil2cfg.node * Cil_types.stmt *
(Cil_types.identified_predicate, Cil_types.identified_term)
Cil_types.behavior)
list * HdefAnnotBhv.t
val find_behaviors : Cil_types.kernel_function ->
Cil2cfg.t ->
Cil_types.kinstr option ->
string list -> HdefAnnotBhv.t * asked_bhv list
empty bhv_names
means all (whatever ki
is)
val process_unreached_annots : Cil2cfg.t -> unit
val get_cfg : Kernel_function.t -> Cil2cfg.t
val build_configs : asked_assigns ->
Kernel_function.t ->
string list ->
Cil_types.kinstr option -> asked_prop -> strategy_info list
val get_strategies : asked_assigns ->
Kernel_function.t ->
string list ->
Cil_types.kinstr option -> asked_prop -> WpStrategy.strategy list
val get_precond_strategies : Property.t -> WpStrategy.strategy list
val get_call_pre_strategies : Cil_datatype.Stmt.t -> WpStrategy.strategy list
val get_id_prop_strategies : ?assigns:asked_assigns -> Property.t -> WpStrategy.strategy list
val get_function_strategies : ?assigns:asked_assigns ->
?bhv:string list ->
?prop:string list -> Kernel_function.t -> WpStrategy.strategy list