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