frama-c-wp.core
LogicCompiler.Make
Pdg_types
frama-c-alias.core
frama-c-aorai.core
frama-c-api-generator.core
frama-c-callgraph.core
frama-c-constant_propagation.core
frama-c-dive.core
frama-c-e-acsl.core
frama-c-eva.core
frama-c-eva.gui
frama-c-from.core
frama-c-from.gui
frama-c-impact.core
frama-c-impact.gui
frama-c-inout.core
frama-c-instantiate.core
frama-c-loop-analysis.core
frama-c-markdown-report.core
frama-c-markdown-report.eva-info
frama-c-metrics.core
frama-c-metrics.gui
frama-c-nonterm.core
frama-c-obfuscator.core
frama-c-occurrence.core
frama-c-occurrence.gui
frama-c-pdg.core
frama-c-pdg.types
frama-c-postdominators.core
frama-c-reduc.core
frama-c-report.core
frama-c-rtegen.core
frama-c-rtegen.gui
frama-c-scope.core
frama-c-scope.gui
frama-c-security_slicing.core
frama-c-security_slicing.gui
frama-c-server.core
frama-c-slicing.core
frama-c-slicing.gui
frama-c-sparecode.core
frama-c-studia.core
frama-c-studia.gui
frama-c-users.core
frama-c-variadic.core
frama-c-wp.gui
frama-c.analysis-scripts
frama-c.boot
frama-c.gui
frama-c.init
frama-c.kernel
frama_c_very_first_cmdline
frama_c_very_first_gui
markdown_report_eva_info
qed
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
type call
type frame
val pp_frame : 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_pre : sigma -> call -> sigma -> frame
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 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
type env
val mk_env : ?here:sigma -> ?lvars:Frama_c_kernel.Cil_datatype.Logic_var.t list -> unit -> env
val current : env -> sigma
val move_at : env -> sigma -> 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