Module WpAnnot

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 = 
| Noproof
| Complete
| Parts of Bitvector.t
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 = 
| FunBhv of Cil_types.funbehavior option
| StmtBhv of Cil2cfg.node * Cil_types.stmt * Cil_types.funbehavior
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 (*
No specified property means all
*)
module HdefAnnotBhv: Cil2cfg.HE(sig
type t = Cil_types.stmt * int 
end)
type strategy_info = {
   kf : Kernel_function.t;
   cfg : Cil2cfg.t;
   cur_bhv : asked_bhv;
   asked_bhvs : asked_bhv list;
   asked_prop : asked_prop;
   assigns_filter : asked_assigns;
   def_annots_info : HdefAnnotBhv.t;
}
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:
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:
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