sig
type scope =
SC_Global
| SC_Frame_in
| SC_Frame_out
| SC_Block_in
| SC_Block_out
module type Export =
sig
type pred
type decl
val export_section : Stdlib.Format.formatter -> string -> unit
val export_goal :
Stdlib.Format.formatter -> string -> Wp.Mcfg.Export.pred -> unit
val export_decl :
Stdlib.Format.formatter -> Wp.Mcfg.Export.decl -> unit
end
module type Splitter =
sig
type pred
val simplify : Wp.Mcfg.Splitter.pred -> Wp.Mcfg.Splitter.pred
val split :
bool -> Wp.Mcfg.Splitter.pred -> Wp.Mcfg.Splitter.pred Bag.t
end
module type S =
sig
type t_env
type t_prop
val pretty : Stdlib.Format.formatter -> Wp.Mcfg.S.t_prop -> unit
val merge :
Wp.Mcfg.S.t_env ->
Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val empty : Wp.Mcfg.S.t_prop
val new_env :
?lvars:Cil_types.logic_var list ->
Cil_types.kernel_function -> Wp.Mcfg.S.t_env
val add_axiom :
Wp.WpPropId.prop_id -> Wp.LogicUsage.logic_lemma -> unit
val add_hyp :
Wp.Mcfg.S.t_env ->
Wp.WpPropId.pred_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val add_goal :
Wp.Mcfg.S.t_env ->
Wp.WpPropId.pred_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val add_assigns :
Wp.Mcfg.S.t_env ->
Wp.WpPropId.assigns_info -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val use_assigns :
Wp.Mcfg.S.t_env ->
Cil_types.stmt option ->
Wp.WpPropId.prop_id option ->
Wp.WpPropId.assigns_desc -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val label :
Wp.Mcfg.S.t_env ->
Cil_types.stmt option ->
Wp.Clabels.c_label -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val init :
Wp.Mcfg.S.t_env ->
Cil_types.varinfo ->
Cil_types.init option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val const :
Wp.Mcfg.S.t_env ->
Cil_types.varinfo -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val assign :
Wp.Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_types.exp -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val return :
Wp.Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.exp option -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val test :
Wp.Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.exp ->
Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val switch :
Wp.Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.exp ->
(Cil_types.exp list * Wp.Mcfg.S.t_prop) list ->
Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val has_init : Wp.Mcfg.S.t_env -> bool
val loop_entry : Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val loop_step : Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val call_dynamic :
Wp.Mcfg.S.t_env ->
Cil_types.stmt ->
Wp.WpPropId.prop_id ->
Cil_types.exp ->
(Cil_types.kernel_function * Wp.Mcfg.S.t_prop) list ->
Wp.Mcfg.S.t_prop
val call_goal_precond :
Wp.Mcfg.S.t_env ->
Cil_types.stmt ->
Cil_types.kernel_function ->
Cil_types.exp list ->
pre:Wp.WpPropId.pred_info list ->
Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val call :
Wp.Mcfg.S.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:Wp.Mcfg.S.t_prop ->
p_exit:Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val scope :
Wp.Mcfg.S.t_env ->
Cil_types.varinfo list ->
Wp.Mcfg.scope -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val close : Wp.Mcfg.S.t_env -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
val build_prop_of_from :
Wp.Mcfg.S.t_env ->
Wp.WpPropId.pred_info list -> Wp.Mcfg.S.t_prop -> Wp.Mcfg.S.t_prop
end
end