sig
type scope =
SC_Global
| SC_Function_in
| SC_Function_frame
| SC_Function_out
| SC_Block_in
| SC_Block_out
module type Export =
sig
type pred
type decl
val export_section : Format.formatter -> string -> unit
val export_goal :
Format.formatter -> string -> Mcfg.Export.pred -> unit
val export_decl : Format.formatter -> Mcfg.Export.decl -> unit
end
module type Splitter =
sig
type pred
val simplify : Mcfg.Splitter.pred -> Mcfg.Splitter.pred
val split : bool -> Mcfg.Splitter.pred -> Mcfg.Splitter.pred Bag.t
end
module type S =
sig
type t_env
type t_prop
val pretty : 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_assigns :
Mcfg.S.t_env ->
WpPropId.assigns_info -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val use_assigns :
Mcfg.S.t_env ->
Cil_types.stmt option ->
WpPropId.prop_id option ->
WpPropId.assigns_desc -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val label :
Mcfg.S.t_env -> Clabels.c_label -> 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 init_value :
Mcfg.S.t_env ->
Cil_types.lval ->
Cil_types.typ ->
Cil_types.exp option -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val init_range :
Mcfg.S.t_env ->
Cil_types.lval ->
Cil_types.typ ->
Integer.t ->
Integer.t -> Cil_types.exp option -> Mcfg.S.t_prop -> Mcfg.S.t_prop
val init_const :
Mcfg.S.t_env -> Cil_types.varinfo -> Mcfg.S.t_prop -> Mcfg.S.t_prop
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 :
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.identified_term 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
end