functor (M : Memory.Model) ->
sig
type value = M.loc Memory.value
type logic = M.loc Memory.logic
type sigma = M.Sigma.t
type chunk = M.Chunk.t
type call
type frame
val pp_frame : Format.formatter -> LogicCompiler.Make.frame -> unit
val frame : Cil_types.kernel_function -> LogicCompiler.Make.frame
val call :
Cil_types.kernel_function ->
LogicCompiler.Make.value list -> LogicCompiler.Make.call
val call_pre :
LogicCompiler.Make.sigma ->
LogicCompiler.Make.call ->
LogicCompiler.Make.sigma -> LogicCompiler.Make.frame
val call_post :
LogicCompiler.Make.sigma ->
LogicCompiler.Make.call ->
LogicCompiler.Make.sigma Memory.sequence -> LogicCompiler.Make.frame
val formal : Cil_types.varinfo -> LogicCompiler.Make.value option
val return : unit -> Cil_types.typ
val result : unit -> Lang.F.var
val status : unit -> Lang.F.var
val trigger : Definitions.trigger -> unit
val guards : LogicCompiler.Make.frame -> Lang.F.pred list
val mem_frame : Clabels.c_label -> LogicCompiler.Make.sigma
val mem_at_frame :
LogicCompiler.Make.frame -> Clabels.c_label -> LogicCompiler.Make.sigma
val in_frame : LogicCompiler.Make.frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> LogicCompiler.Make.frame
type env
val new_env : Cil_datatype.Logic_var.t list -> LogicCompiler.Make.env
val move :
LogicCompiler.Make.env ->
LogicCompiler.Make.sigma -> LogicCompiler.Make.env
val sigma : LogicCompiler.Make.env -> LogicCompiler.Make.sigma
val env_at :
LogicCompiler.Make.env -> Clabels.c_label -> LogicCompiler.Make.env
val mem_at :
LogicCompiler.Make.env -> Clabels.c_label -> LogicCompiler.Make.sigma
val env_let :
LogicCompiler.Make.env ->
Cil_types.logic_var ->
LogicCompiler.Make.logic -> LogicCompiler.Make.env
val env_letp :
LogicCompiler.Make.env ->
Cil_types.logic_var -> Lang.F.pred -> LogicCompiler.Make.env
val env_letval :
LogicCompiler.Make.env ->
Cil_types.logic_var ->
LogicCompiler.Make.value -> LogicCompiler.Make.env
val term : LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term
val pred :
LogicCompiler.polarity ->
LogicCompiler.Make.env -> Cil_types.predicate -> Lang.F.pred
val logic :
LogicCompiler.Make.env -> Cil_types.term -> LogicCompiler.Make.logic
val region :
LogicCompiler.Make.env -> Cil_types.term -> M.loc Memory.sloc list
val bootstrap_term :
(LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term) -> unit
val bootstrap_pred :
(LogicCompiler.polarity ->
LogicCompiler.Make.env -> Cil_types.predicate -> Lang.F.pred) ->
unit
val bootstrap_logic :
(LogicCompiler.Make.env -> Cil_types.term -> LogicCompiler.Make.logic) ->
unit
val bootstrap_region :
(LogicCompiler.Make.env -> Cil_types.term -> M.loc Memory.sloc list) ->
unit
val call_fun :
LogicCompiler.Make.env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.term
val call_pred :
LogicCompiler.Make.env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.pred
val logic_var :
LogicCompiler.Make.env ->
Cil_types.logic_var -> LogicCompiler.Make.logic
val logic_info :
LogicCompiler.Make.env -> Cil_types.logic_info -> Lang.F.pred option
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
end