Module type Wp.Mcfg.S

module type S = sig .. end

This is what is really needed to propagate something through the CFG. Usually, the propagated thing should be a predicate, but it can be more sophisticated like lists of predicates, or maybe a structure to keep hypotheses and goals separated. Moreover, proof obligations may also need to be handled.


type t_env 
type t_prop 
val pretty : Stdlib.Format.formatter -> t_prop -> unit
val merge : t_env -> t_prop -> t_prop -> t_prop
val empty : t_prop
val new_env : ?lvars:Cil_types.logic_var list ->
Cil_types.kernel_function -> t_env

optionally init env with user logic variables

val add_axiom : Wp.WpPropId.prop_id -> Wp.LogicUsage.logic_lemma -> unit
val add_hyp : t_env ->
Wp.WpPropId.pred_info -> t_prop -> t_prop
val add_goal : t_env ->
Wp.WpPropId.pred_info -> t_prop -> t_prop
val add_subgoal : t_env ->
Wp.WpPropId.pred_info ->
?deps:Property.Set.t ->
Cil_types.predicate ->
Cil_types.stmt ->
Wp.WpPropId.effect_source -> t_prop -> t_prop
val add_assigns : t_env ->
Wp.WpPropId.assigns_info -> t_prop -> t_prop
val use_assigns : t_env ->
Wp.WpPropId.prop_id option ->
Wp.WpPropId.assigns_desc -> t_prop -> t_prop

use_assigns env hid kind assgn goal performs the havoc on the goal. hid should be None iff assgn is WritesAny, and tied to the corresponding identified_property otherwise.

val label : t_env ->
Cil_types.stmt option ->
Wp.Clabels.c_label -> t_prop -> t_prop
val init : t_env ->
Cil_types.varinfo ->
Cil_types.init option -> t_prop -> t_prop
val const : t_env -> Cil_types.varinfo -> t_prop -> t_prop
val assign : t_env ->
Cil_types.stmt ->
Cil_types.lval -> Cil_types.exp -> t_prop -> t_prop
val return : t_env ->
Cil_types.stmt ->
Cil_types.exp option -> t_prop -> t_prop
val test : t_env ->
Cil_types.stmt ->
Cil_types.exp -> t_prop -> t_prop -> t_prop
val switch : t_env ->
Cil_types.stmt ->
Cil_types.exp ->
(Cil_types.exp list * t_prop) list ->
t_prop -> t_prop
val has_init : t_env -> bool
val loop_entry : t_prop -> t_prop
val loop_step : t_prop -> t_prop
val call_dynamic : t_env ->
Cil_types.stmt ->
Wp.WpPropId.prop_id ->
Cil_types.exp ->
(Cil_types.kernel_function * t_prop) list -> t_prop
val call_goal_precond : t_env ->
Cil_types.stmt ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:Wp.WpPropId.pred_info list -> t_prop -> t_prop
val call_terminates : t_env ->
Wp.WpPropId.pred_info ->
Cil_types.stmt ->
Cil_types.kernel_function ->
Cil_types.exp list ->
callee_t:Cil_types.predicate -> t_prop -> t_prop
val call : t_env ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:Wp.WpPropId.pred_info list ->
post:Wp.WpPropId.pred_info list ->
pexit:Wp.WpPropId.pred_info list ->
assigns:Cil_types.assigns ->
p_post:t_prop -> p_exit:t_prop -> t_prop
val scope : t_env ->
Cil_types.varinfo list ->
Wp.Mcfg.scope -> t_prop -> t_prop
val close : t_env -> t_prop -> t_prop
val build_prop_of_from : t_env ->
Wp.WpPropId.pred_info list -> t_prop -> t_prop

build p => alpha(p) for functional dependencies verification.