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 signature =
CST of Integer.t
| SIG of LogicCompiler.Make.sig_param list
and sig_param =
Sig_value of Cil_types.logic_var
| Sig_chunk of LogicCompiler.Make.chunk * Clabels.c_label
val wrap_lvar :
Cil_datatype.Logic_var.Map.key list ->
'a list -> 'a Cil_datatype.Logic_var.Map.t
val wrap_var :
Cil_datatype.Varinfo.Map.key list ->
'a list -> 'a Cil_datatype.Varinfo.Map.t
val wrap_mem : (Clabels.LabelMap.key * 'a) list -> 'a Clabels.LabelMap.t
val fresh_lvar : ?basename:string -> Cil_types.logic_type -> Lang.F.var
val fresh_cvar : ?basename:string -> Cil_types.typ -> Lang.F.var
type frame = {
name : string;
pool : Lang.F.pool;
gamma : Lang.gamma;
kf : Cil_types.kernel_function option;
formals : LogicCompiler.Make.value Cil_datatype.Varinfo.Map.t;
types : string list;
mutable triggers : Definitions.trigger list;
mutable labels : LogicCompiler.Make.sigma Clabels.LabelMap.t;
mutable result : Lang.F.var option;
mutable status : Lang.F.var option;
}
val pp_frame : Format.formatter -> LogicCompiler.Make.frame -> unit
val logic_frame : string -> string list -> LogicCompiler.Make.frame
val frame : Kernel_function.t -> LogicCompiler.Make.frame
val call_pre :
Kernel_function.t ->
LogicCompiler.Make.value list ->
LogicCompiler.Make.sigma -> LogicCompiler.Make.frame
val call_post :
Kernel_function.t ->
LogicCompiler.Make.value list ->
LogicCompiler.Make.sigma Memory.sequence -> LogicCompiler.Make.frame
val frame_copy : LogicCompiler.Make.frame -> LogicCompiler.Make.frame
val cframe : LogicCompiler.Make.frame Context.value
val get_frame : unit -> LogicCompiler.Make.frame
val in_frame : LogicCompiler.Make.frame -> ('a -> 'b) -> 'a -> 'b
val mem_at_frame :
LogicCompiler.Make.frame ->
Clabels.LabelMap.key -> LogicCompiler.Make.sigma
val mem_frame : Clabels.LabelMap.key -> LogicCompiler.Make.sigma
val formal :
Cil_datatype.Varinfo.Map.key -> 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
type env = {
vars : LogicCompiler.Make.logic Cil_datatype.Logic_var.Map.t;
lhere : LogicCompiler.Make.sigma option;
current : LogicCompiler.Make.sigma option;
}
val plain_of_exp : Cil_types.logic_type -> Lang.F.term -> 'a Memory.logic
val new_env :
Cil_datatype.Logic_var.Map.key list -> LogicCompiler.Make.env
val sigma : LogicCompiler.Make.env -> LogicCompiler.Make.sigma
val move :
LogicCompiler.Make.env ->
LogicCompiler.Make.sigma -> LogicCompiler.Make.env
val env_at :
LogicCompiler.Make.env ->
Clabels.LabelMap.key -> LogicCompiler.Make.env
val mem_at :
LogicCompiler.Make.env ->
Clabels.LabelMap.key -> LogicCompiler.Make.sigma
val env_let :
LogicCompiler.Make.env ->
Cil_datatype.Logic_var.Map.key ->
LogicCompiler.Make.logic -> LogicCompiler.Make.env
val env_letval :
LogicCompiler.Make.env ->
Cil_datatype.Logic_var.Map.key ->
M.loc Memory.value -> LogicCompiler.Make.env
val param_of_lv : Cil_types.logic_var -> Lang.F.var
val profile_env :
LogicCompiler.Make.logic Cil_datatype.Logic_var.Map.t ->
(Cil_datatype.Logic_var.Map.key * Lang.F.var) list ->
Cil_datatype.Logic_var.Map.key list ->
LogicCompiler.Make.env *
(Cil_datatype.Logic_var.Map.key * Lang.F.var) list
val default_label :
LogicCompiler.Make.env ->
Cil_types.logic_label list -> LogicCompiler.Make.env
val compile_step :
string ->
string list ->
Cil_types.logic_var list ->
Cil_types.logic_label list ->
(LogicCompiler.Make.env -> 'a -> 'b) ->
('b -> Lang.F.var -> bool) ->
'a ->
Lang.F.var list * Definitions.trigger list * 'b *
LogicCompiler.Make.sig_param list
val cc_term :
(LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term)
Pervasives.ref
val cc_pred :
(bool ->
LogicCompiler.Make.env ->
Cil_types.predicate Cil_types.named -> Lang.F.pred)
Pervasives.ref
val cc_logic :
(LogicCompiler.Make.env -> Cil_types.term -> LogicCompiler.Make.logic)
Pervasives.ref
val cc_region :
(LogicCompiler.Make.env -> Cil_types.term -> M.loc Memory.sloc list)
Pervasives.ref
val term : LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term
val pred :
bool ->
LogicCompiler.Make.env ->
Cil_types.predicate Cil_types.named -> 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 reads :
LogicCompiler.Make.env -> Cil_types.identified_term list -> unit
val bootstrap_term :
(LogicCompiler.Make.env -> Cil_types.term -> Lang.F.term) -> unit
val bootstrap_pred :
(bool ->
LogicCompiler.Make.env ->
Cil_types.predicate Cil_types.named -> 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 in_term : Lang.F.term -> Lang.F.var -> bool
val in_pred : Lang.F.pred -> Lang.F.var -> bool
val in_reads : 'a -> 'b -> bool
val is_recursive : Cil_types.logic_info -> Definitions.recursion
module Axiomatic :
sig
module E :
sig
type key = string
type data = unit
val name : string
val compare : key -> key -> int
val pretty : Format.formatter -> key -> unit
end
type key = E.key
type data = E.data
val mem : key -> bool
val find : key -> data
val get : key -> data option
val define : key -> data -> unit
val update : key -> data -> unit
val memoize : (key -> data) -> key -> data
val compile : (key -> data) -> key -> unit
val callback : (key -> data -> unit) -> unit
val iter : (key -> data -> unit) -> unit
val iter_sorted : (key -> data -> unit) -> unit
end
module Signature :
sig
module E :
sig
type key = Cil_types.logic_info
type data = signature
val name : string
val compare : key -> key -> int
val pretty : Format.formatter -> key -> unit
end
type key = E.key
type data = E.data
val mem : key -> bool
val find : key -> data
val get : key -> data option
val define : key -> data -> unit
val update : key -> data -> unit
val memoize : (key -> data) -> key -> data
val compile : (key -> data) -> key -> unit
val callback : (key -> data -> unit) -> unit
val iter : (key -> data -> unit) -> unit
val iter_sorted : (key -> data -> unit) -> unit
end
val compile_lemma :
Definitions.cluster ->
string ->
assumed:bool ->
string list ->
Cil_types.logic_label list ->
Cil_types.predicate Cil_types.named -> Definitions.dlemma
val type_for_signature :
Cil_types.logic_info ->
Definitions.dfun -> LogicCompiler.Make.sig_param list -> unit
val compile_lbpure :
Definitions.cluster ->
LogicCompiler.Make.Signature.key ->
Lang.F.var list * LogicCompiler.Make.sig_param list
val compile_lbnone :
Definitions.cluster ->
Cil_types.logic_info ->
Cil_types.varinfo list -> LogicCompiler.Make.signature
val compile_lbreads :
Definitions.cluster ->
Cil_types.logic_info ->
Cil_types.identified_term list -> LogicCompiler.Make.signature
val compile_rec :
string ->
LogicCompiler.Make.Signature.key ->
(LogicCompiler.Make.env -> 'a -> 'b) ->
('b -> Lang.F.var -> bool) ->
'a ->
Lang.F.var list * Definitions.trigger list * 'b *
LogicCompiler.Make.sig_param list
val compile_lbterm :
Definitions.cluster ->
LogicCompiler.Make.Signature.key ->
Cil_types.term -> LogicCompiler.Make.signature
val compile_lbpred :
Definitions.cluster ->
LogicCompiler.Make.Signature.key ->
Cil_types.predicate Cil_types.named -> LogicCompiler.Make.signature
val heap_case :
Clabels.LabelSet.t Clabels.LabelMap.t ->
Clabels.LabelSet.t M.Heap.Map.t ->
LogicCompiler.Make.sig_param -> Clabels.LabelSet.t M.Heap.Map.t
val compile_lbinduction :
Definitions.cluster ->
LogicCompiler.Make.Signature.key ->
(string * Cil_types.logic_label list * string list *
Cil_types.predicate Cil_types.named)
list -> LogicCompiler.Make.signature
val compile_logic :
Definitions.cluster ->
LogicUsage.logic_section ->
LogicCompiler.Make.Signature.key -> LogicCompiler.Make.signature
val define_type :
Definitions.cluster -> Cil_types.logic_type_info -> unit
val define_logic :
Definitions.cluster ->
LogicUsage.logic_section -> LogicCompiler.Make.Signature.key -> unit
val define_lemma : Definitions.cluster -> LogicUsage.logic_lemma -> unit
val define_axiomatic :
Definitions.cluster -> LogicUsage.axiomatic -> unit
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
val signature :
LogicCompiler.Make.Signature.key -> LogicCompiler.Make.Signature.data
val bind_labels :
LogicCompiler.Make.env ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
LogicCompiler.Make.sigma Clabels.LabelMap.t
val call_params :
LogicCompiler.Make.env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
LogicCompiler.Make.sig_param list ->
Lang.F.term list -> Lang.F.term list
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_datatype.Logic_var.Map.key -> LogicCompiler.Make.logic
end