functor (W : Mcfg.S) ->
sig
val dkey : Log.category
val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
val do_labels : W.t_env -> Cil2cfg.edge -> W.t_prop -> W.t_prop
val add_hyp : W.t_env -> W.t_prop -> WpPropId.pred_info -> W.t_prop
val open_scope :
W.t_env -> Cil_types.varinfo list -> Cil_types.block list -> W.t_prop
val add_goal : W.t_env -> W.t_prop -> WpPropId.pred_info -> W.t_prop
val add_assigns_goal :
W.t_env -> W.t_prop -> WpPropId.assigns_full_info -> W.t_prop
val add_assigns_hyp :
W.t_env ->
W.t_prop ->
WpPropId.assigns_full_info -> Clabels.c_label option * W.t_prop
exception Stop of Cil2cfg.edge
val test_edge_loop_ok :
Cil2cfg.t -> WpStrategy.strategy option -> Cil2cfg.Eset.elt -> bool
module R :
sig
type t
val empty : Cil2cfg.t -> Calculus.Cfg.??.t
val is_pass1 : Calculus.Cfg.??.t -> bool
val change_mode_if_needed : Calculus.Cfg.??.t -> unit
val find : Calculus.Cfg.??.t -> Cil2cfg.edge -> W.t_prop
val set :
WpStrategy.strategy ->
W.t_env ->
Calculus.Cfg.??.t -> Cil2cfg.edge -> W.t_prop -> W.t_prop
val add_oblig :
Calculus.Cfg.??.t -> Clabels.c_label -> W.t_prop -> unit
val add_memo : Calculus.Cfg.??.t -> Cil2cfg.edge -> W.t_prop -> unit
end
val use_loop_assigns :
WpStrategy.strategy -> W.t_env -> Cil2cfg.edge -> W.t_prop -> W.t_prop
val loop_with_cut :
Cil2cfg.t -> WpStrategy.strategy -> Cil2cfg.node -> bool
val wp_loop :
'a * Cil2cfg.t * WpStrategy.strategy * 'b * W.t_env ->
Calculus.Cfg.R.t ->
Cil2cfg.node -> Cil2cfg.edge -> (Cil2cfg.node -> W.t_prop) -> W.t_prop
type callenv = {
pre_annots : WpStrategy.t_annots;
post_annots : WpStrategy.t_annots;
exit_annots : WpStrategy.t_annots;
}
val callenv :
Cil2cfg.t ->
WpStrategy.strategy -> Cil2cfg.node -> Calculus.Cfg.callenv
val wp_call_any :
W.t_env ->
Calculus.Cfg.callenv -> p_post:W.t_prop -> p_exit:W.t_prop -> W.t_prop
val wp_call_kf :
W.t_env ->
Calculus.Cfg.callenv ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.kernel_function ->
Cil_types.exp list ->
bool -> p_post:W.t_prop -> p_exit:W.t_prop -> W.t_prop
val wp_calls :
Cil_types.kernel_function * Cil2cfg.t * WpStrategy.strategy * 'a *
W.t_env ->
Calculus.Cfg.R.t ->
Cil2cfg.node ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil2cfg.call_type ->
Cil_types.exp list -> W.t_prop -> W.t_prop -> W.t_prop
val wp_stmt : W.t_env -> Cil_types.stmt -> W.t_prop -> W.t_prop
val wp_scope :
W.t_env -> Cil_types.varinfo list -> Mcfg.scope -> W.t_prop -> W.t_prop
val get_wp_edge :
Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
Calculus.Cfg.R.t * W.t_env -> Cil2cfg.Eset.elt -> W.t_prop
val get_only_succ :
Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
Calculus.Cfg.R.t * W.t_env -> Cil2cfg.t -> Cil2cfg.node -> W.t_prop
val compute_wp_edge :
Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
Calculus.Cfg.R.t * W.t_env -> Cil2cfg.Eset.elt -> W.t_prop
val init_global_variable :
W.t_env -> Cil_types.lval -> Cil_types.init -> W.t_prop -> W.t_prop
val process_global_init :
W.t_env -> Cil_types.kernel_function -> W.t_prop -> W.t_prop
val get_weakest_precondition :
Cil2cfg.t ->
Kernel_function.t * Cil2cfg.t * WpStrategy.strategy *
Calculus.Cfg.R.t * W.t_env -> W.t_prop
val compute :
Cil2cfg.t ->
WpStrategy.strategy ->
W.t_prop list * (Format.formatter -> Cil2cfg.edge -> unit)
end