sig
type polarity = [ `Negative | `NoPolarity | `Positive ]
module Make :
functor (M : Sigs.Model) ->
sig
type value = M.loc Wp.Sigs.value
type logic = M.loc Wp.Sigs.logic
type result = M.loc Wp.Sigs.result
type sigma = M.Sigma.t
type chunk = M.Chunk.t
type call
type frame
val pp_frame :
Stdlib.Format.formatter -> Wp.LogicCompiler.Make.frame -> unit
val local : descr:string -> Wp.LogicCompiler.Make.frame
val frame : Cil_types.kernel_function -> Wp.LogicCompiler.Make.frame
val call :
?result:M.loc ->
Cil_types.kernel_function ->
Wp.LogicCompiler.Make.value list -> Wp.LogicCompiler.Make.call
val call_pre :
Wp.LogicCompiler.Make.sigma ->
Wp.LogicCompiler.Make.call ->
Wp.LogicCompiler.Make.sigma -> Wp.LogicCompiler.Make.frame
val call_post :
Wp.LogicCompiler.Make.sigma ->
Wp.LogicCompiler.Make.call ->
Wp.LogicCompiler.Make.sigma Wp.Sigs.sequence ->
Wp.LogicCompiler.Make.frame
val mk_frame :
?kf:Cil_types.kernel_function ->
?result:Wp.LogicCompiler.Make.result ->
?status:Wp.Lang.F.var ->
?formals:Wp.LogicCompiler.Make.value Cil_datatype.Varinfo.Map.t ->
?labels:Wp.LogicCompiler.Make.sigma Wp.Clabels.LabelMap.t ->
?descr:string -> unit -> Wp.LogicCompiler.Make.frame
val formal : Cil_types.varinfo -> Wp.LogicCompiler.Make.value option
val return : unit -> Cil_types.typ
val result : unit -> Wp.LogicCompiler.Make.result
val status : unit -> Wp.Lang.F.var
val trigger : Wp.Definitions.trigger -> unit
val guards : Wp.LogicCompiler.Make.frame -> Wp.Lang.F.pred list
val mem_frame : Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
val has_at_frame :
Wp.LogicCompiler.Make.frame -> Wp.Clabels.c_label -> bool
val mem_at_frame :
Wp.LogicCompiler.Make.frame ->
Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
val set_at_frame :
Wp.LogicCompiler.Make.frame ->
Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma -> unit
val in_frame : Wp.LogicCompiler.Make.frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> Wp.LogicCompiler.Make.frame
type env
val mk_env :
?here:Wp.LogicCompiler.Make.sigma ->
?lvars:Cil_datatype.Logic_var.t list ->
unit -> Wp.LogicCompiler.Make.env
val current :
Wp.LogicCompiler.Make.env -> Wp.LogicCompiler.Make.sigma
val move_at :
Wp.LogicCompiler.Make.env ->
Wp.LogicCompiler.Make.sigma -> Wp.LogicCompiler.Make.env
val env_at :
Wp.LogicCompiler.Make.env ->
Wp.Clabels.c_label -> Wp.LogicCompiler.Make.env
val mem_at :
Wp.LogicCompiler.Make.env ->
Wp.Clabels.c_label -> Wp.LogicCompiler.Make.sigma
val env_let :
Wp.LogicCompiler.Make.env ->
Cil_types.logic_var ->
Wp.LogicCompiler.Make.logic -> Wp.LogicCompiler.Make.env
val env_letp :
Wp.LogicCompiler.Make.env ->
Cil_types.logic_var -> Wp.Lang.F.pred -> Wp.LogicCompiler.Make.env
val env_letval :
Wp.LogicCompiler.Make.env ->
Cil_types.logic_var ->
Wp.LogicCompiler.Make.value -> Wp.LogicCompiler.Make.env
val term :
Wp.LogicCompiler.Make.env -> Cil_types.term -> Wp.Lang.F.term
val pred :
Wp.LogicCompiler.polarity ->
Wp.LogicCompiler.Make.env -> Cil_types.predicate -> Wp.Lang.F.pred
val logic :
Wp.LogicCompiler.Make.env ->
Cil_types.term -> Wp.LogicCompiler.Make.logic
val region :
Wp.LogicCompiler.Make.env -> Cil_types.term -> M.loc Wp.Sigs.region
val bootstrap_term :
(Wp.LogicCompiler.Make.env -> Cil_types.term -> Wp.Lang.F.term) ->
unit
val bootstrap_pred :
(Wp.LogicCompiler.polarity ->
Wp.LogicCompiler.Make.env -> Cil_types.predicate -> Wp.Lang.F.pred) ->
unit
val bootstrap_logic :
(Wp.LogicCompiler.Make.env ->
Cil_types.term -> Wp.LogicCompiler.Make.logic) ->
unit
val bootstrap_region :
(Wp.LogicCompiler.Make.env ->
Cil_types.term -> M.loc Wp.Sigs.region) ->
unit
val call_fun :
Wp.LogicCompiler.Make.env ->
Wp.Lang.F.tau ->
Cil_types.logic_info ->
Cil_types.logic_label list -> Wp.Lang.F.term list -> Wp.Lang.F.term
val call_pred :
Wp.LogicCompiler.Make.env ->
Cil_types.logic_info ->
Cil_types.logic_label list -> Wp.Lang.F.term list -> Wp.Lang.F.pred
val logic_var :
Wp.LogicCompiler.Make.env ->
Cil_types.logic_var -> Wp.LogicCompiler.Make.logic
val logic_info :
Wp.LogicCompiler.Make.env ->
Cil_types.logic_info -> Wp.Lang.F.pred option
val has_ltype :
Cil_types.logic_type -> Wp.Lang.F.term -> Wp.Lang.F.pred
val lemma : Wp.LogicUsage.logic_lemma -> Wp.Definitions.dlemma
end
end