Frama-C:
Plug-ins:
Libraries:

Frama-C API - Make

Parameters

module M : Memory.Model

Signature

Definitions

type value = M.loc Memory.value
type logic = M.loc Memory.logic
type result = M.loc Memory.result

Frames

type call
type frame
val pp_frame : Stdlib.Format.formatter -> frame -> unit
val local : descr:string -> frame
val call : ?result:M.loc -> Frama_c_kernel.Cil_types.kernel_function -> value list -> call
val call_pre : Sigma.sigma -> call -> Sigma.sigma -> frame
val call_post : Sigma.sigma -> call -> Sigma.sigma Memory.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.sigma Wp__.Clabels.LabelMap.t -> ?descr:string -> unit -> frame
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.sigma
val has_at_frame : frame -> Clabels.c_label -> bool
val mem_at_frame : frame -> Clabels.c_label -> Sigma.sigma
val set_at_frame : frame -> Clabels.c_label -> Sigma.sigma -> unit
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
val get_frame : unit -> frame

Environment

type env
val mk_env : ?here:Sigma.sigma -> ?lvars:Frama_c_kernel.Cil_datatype.Logic_var.t list -> unit -> env
val current : env -> Sigma.sigma
val move_at : env -> Sigma.sigma -> env
val env_at : env -> Clabels.c_label -> env
val mem_at : env -> Clabels.c_label -> Sigma.sigma

Compiler

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 Memory.region) -> unit

Application

Logic Variable and ACSL Constants

Logic Lemmas