Functor LogicCompiler.Make

module Make: 
functor (M : Memory.Model) -> sig .. end
Parameters:
M : Memory.Model

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 sig_param list
type sig_param = 
| Sig_value of Cil_types.logic_var
| Sig_chunk of 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 : value Cil_datatype.Varinfo.Map.t;
   types : string list;
   mutable triggers : Definitions.trigger list;
   mutable labels : sigma Clabels.LabelMap.t;
   mutable result : Lang.F.var option;
   mutable status : Lang.F.var option;
}
val pp_frame : Format.formatter -> frame -> unit
val logic_frame : string -> string list -> frame
val frame : Kernel_function.t -> frame
val call_pre : sigma ->
Kernel_function.t ->
value list ->
sigma -> frame
val call_post : sigma ->
Kernel_function.t ->
value list ->
sigma Memory.sequence -> frame
val frame_copy : frame -> frame
val cframe : frame Context.value
val get_frame : unit -> frame
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val mem_at_frame : frame -> Clabels.LabelMap.key -> sigma
val mem_frame : Clabels.LabelMap.key -> sigma
val formal : Cil_datatype.Varinfo.Map.key -> 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 : frame -> Lang.F.pred list
type env = {
   vars : logic Cil_datatype.Logic_var.Map.t;
   lhere : sigma option;
   current : 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 -> env
val sigma : env -> sigma
val move : env -> sigma -> env
val env_at : env -> Clabels.LabelMap.key -> env
val mem_at : env -> Clabels.LabelMap.key -> sigma
val env_let : env ->
Cil_datatype.Logic_var.Map.key ->
logic -> env
val env_letval : env ->
Cil_datatype.Logic_var.Map.key ->
M.loc Memory.value -> env
val param_of_lv : Cil_types.logic_var -> Lang.F.var
val profile_env : logic Cil_datatype.Logic_var.Map.t ->
Lang.F.pred list ->
(Cil_datatype.Logic_var.Map.key * Lang.F.var) list ->
Cil_datatype.Logic_var.Map.key list ->
env * Lang.F.pred list *
(Cil_datatype.Logic_var.Map.key * Lang.F.var) list
val default_label : env ->
Cil_types.logic_label list -> env
val compile_step : string ->
string list ->
Cil_types.logic_var list ->
Cil_types.logic_label list ->
(env -> 'a -> 'b) ->
('b -> Lang.F.var -> bool) ->
'a ->
Lang.F.var list * Definitions.trigger list * Lang.F.pred list * 'b *
sig_param list
val cc_term : (env -> Cil_types.term -> Lang.F.term) Pervasives.ref
val cc_pred : (bool ->
env -> Cil_types.predicate Cil_types.named -> Lang.F.pred)
Pervasives.ref
val cc_logic : (env -> Cil_types.term -> logic)
Pervasives.ref
val cc_region : (env -> Cil_types.term -> M.loc Memory.sloc list)
Pervasives.ref
val term : env -> Cil_types.term -> Lang.F.term
val pred : bool ->
env -> Cil_types.predicate Cil_types.named -> Lang.F.pred
val logic : env -> Cil_types.term -> logic
val region : env -> Cil_types.term -> M.loc Memory.sloc list
val reads : env -> Cil_types.identified_term list -> unit
val bootstrap_term : (env -> Cil_types.term -> Lang.F.term) -> unit
val bootstrap_pred : (bool ->
env -> Cil_types.predicate Cil_types.named -> Lang.F.pred) ->
unit
val bootstrap_logic : (env -> Cil_types.term -> logic) ->
unit
val bootstrap_region : (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: Model.Index(sig
type key = string 
type data = unit 
val name : string
val compare : String.t -> String.t -> int
val pretty : Format.formatter -> string -> unit
end)
module Signature: Model.Index(sig
type key = Cil_types.logic_info 
type data = LogicCompiler.Make.signature 
val name : string
val compare : Cil_datatype.Logic_info.t -> Cil_datatype.Logic_info.t -> int
val pretty : Format.formatter -> Cil_types.logic_info -> unit
end)
val strip_forall : Cil_types.logic_var list ->
Cil_types.predicate Cil_types.named ->
Cil_types.logic_var list * Cil_types.predicate Cil_types.named
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 -> sig_param list -> unit
val compile_lbpure : Definitions.cluster ->
Signature.key ->
Lang.F.var list * sig_param list
val compile_lbnone : Definitions.cluster ->
Cil_types.logic_info ->
Cil_types.varinfo list -> signature
val compile_lbreads : Definitions.cluster ->
Cil_types.logic_info ->
Cil_types.identified_term list -> signature
val compile_rec : string ->
Signature.key ->
(env -> 'a -> 'b) ->
('b -> Lang.F.var -> bool) ->
'a ->
Lang.F.var list * Definitions.trigger list * Lang.F.pred list * 'b *
sig_param list
val compile_lbterm : Definitions.cluster ->
Signature.key ->
Cil_types.term -> signature
val compile_lbpred : Definitions.cluster ->
Signature.key ->
Cil_types.predicate Cil_types.named -> signature
val heap_case : Clabels.LabelSet.t Clabels.LabelMap.t ->
Clabels.LabelSet.t M.Heap.Map.t ->
sig_param -> Clabels.LabelSet.t M.Heap.Map.t
val compile_lbinduction : Definitions.cluster ->
Signature.key ->
(string * Cil_types.logic_label list * string list *
Cil_types.predicate Cil_types.named)
list -> signature
val compile_logic : Definitions.cluster ->
LogicUsage.logic_section ->
Signature.key -> signature
val define_type : Definitions.cluster -> Cil_types.logic_type_info -> unit
val define_logic : Definitions.cluster ->
LogicUsage.logic_section -> 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 : Signature.key -> Signature.data
val bind_labels : env ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
sigma Clabels.LabelMap.t
val call_params : env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
sig_param list -> Lang.F.term list -> Lang.F.term list
val call_fun : env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.term
val call_pred : env ->
Cil_types.logic_info ->
(Cil_types.logic_label * Cil_types.logic_label) list ->
Lang.F.term list -> Lang.F.pred
val logic_var : env ->
Cil_datatype.Logic_var.Map.key -> logic