Module CfgDump.WP

module WP: Calculus.Cfg(VC)

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
Before storing something at a program point, we have to process the label at that point.
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
detect if the computation of the result at edge is possible, or if it will loop. If strategy are provide, cut are done on edges with cut properties, and if not, cut are done on loop node back edge if any. TODO: maybe this should be done while building the strategy ?
val test_edge_loop_ok : Cil2cfg.t -> WpStrategy.strategy option -> Cil2cfg.Eset.elt -> bool
module R: sig .. end
to store the results of computations : we store a result for each edge, and also a list of proof obligations.
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 ->
R.t ->
Cil2cfg.node -> Cil2cfg.edge -> (Cil2cfg.node -> W.t_prop) -> W.t_prop
Compute the result for edge e which goes to the loop node nloop. So e can be either a back_edge or a loop entry edge. Be very careful not to make an infinite loop by calling get_loop_head...
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 -> callenv
val wp_call_any : W.t_env ->
callenv -> p_post:W.t_prop -> p_exit:W.t_prop -> W.t_prop
val wp_call_kf : W.t_env ->
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 ->
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 * R.t *
W.t_env -> Cil2cfg.Eset.elt -> W.t_prop
Returns the WP stored for edge e. Compute it if it is not already there and store it. Also handle the Acut annotations.
val get_only_succ : Kernel_function.t * Cil2cfg.t * WpStrategy.strategy * R.t *
W.t_env -> Cil2cfg.t -> Cil2cfg.node -> W.t_prop
val compute_wp_edge : Kernel_function.t * Cil2cfg.t * WpStrategy.strategy * 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 * R.t *
W.t_env -> W.t_prop
val compute : Cil2cfg.t ->
WpStrategy.strategy ->
W.t_prop list * (Format.formatter -> Cil2cfg.edge -> unit)