sig
type t_env
type t_prop
val pretty : Stdlib.Format.formatter -> Mcfg.S.t_prop -> unit
val merge : Mcfg.S.t_env -> Mcfg.S.t_prop -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val empty : Mcfg.S.t_prop
val new_env :
?lvars:Cil_types.logic_var list ->
Cil_types.kernel_function -> Mcfg.S.t_env
val add_axiom : WpPropId.prop_id -> LogicUsage.logic_lemma -> unit
val add_hyp :
Mcfg.S.t_env -> WpPropId.pred_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val add_goal :
Mcfg.S.t_env -> WpPropId.pred_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val add_subgoal :
Mcfg.S.t_env ->
WpPropId.pred_info ->
?deps:Property.Set.t ->
Cil_types.predicate ->
Cil_types.stmt ->
WpPropId.effect_source -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val add_assigns :
Mcfg.S.t_env -> WpPropId.assigns_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val use_assigns :
Mcfg.S.t_env ->
WpPropId.prop_id option ->
WpPropId.assigns_desc -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val label :
Mcfg.S.t_env ->
Cil_types.stmt option ->
Clabels.c_label -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val init :
Mcfg.S.t_env ->
Cil_types.varinfo ->
Cil_types.init option -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val const :
Mcfg.S.t_env -> Cil_types.varinfo -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val assign :
Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.lval -> Cil_types.exp -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val return :
Mcfg.S.t_env ->
Cil_types.stmt -> Cil_types.exp option -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val test :
Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.exp -> Mcfg.S.t_prop -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val switch :
Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.exp ->
(Cil_types.exp list * Mcfg.S.t_prop) list ->
Mcfg.S.t_prop -> Mcfg.S.t_prop
val has_init : Mcfg.S.t_env -> bool
val loop_entry : Mcfg.S.t_prop -> Mcfg.S.t_prop
val loop_step : Mcfg.S.t_prop -> Mcfg.S.t_prop
val call_dynamic :
Mcfg.S.t_env ->
Cil_types.stmt ->
WpPropId.prop_id ->
Cil_types.exp ->
(Cil_types.kernel_function * Mcfg.S.t_prop) list -> Mcfg.S.t_prop
val call_goal_precond :
Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:WpPropId.pred_info list -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val call_terminates :
Mcfg.S.t_env ->
WpPropId.pred_info ->
Cil_types.stmt ->
Cil_types.kernel_function ->
Cil_types.exp list ->
callee_t:Cil_types.predicate -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val call :
Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:WpPropId.pred_info list ->
post:WpPropId.pred_info list ->
pexit:WpPropId.pred_info list ->
assigns:Cil_types.assigns ->
p_post:Mcfg.S.t_prop -> p_exit:Mcfg.S.t_prop -> Mcfg.S.t_prop
val scope :
Mcfg.S.t_env ->
Cil_types.varinfo list -> Mcfg.scope -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val close : Mcfg.S.t_env -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val build_prop_of_from :
Mcfg.S.t_env -> WpPropId.pred_info list -> Mcfg.S.t_prop -> Mcfg.S.t_prop
end