Frama-C API - Make
Parameters
module M : Sigs.Model
Signature
module M = M
Underlying memory model
type loc = M.loc
type nonrec value = M.loc Sigs.value
type nonrec logic = M.loc Sigs.logic
type nonrec region = M.loc Sigs.region
type nonrec result = M.loc Sigs.result
type sigma = M.Sigma.t
Frames
Frames are compilation environment for ACSL. A frame typically manages the current function, formal paramters, the memory environments at different labels and the \result
and \exit_status
values.
The frame also holds the gamma environment responsible for accumulating typing constraints, and the pool for generating fresh logic variables.
Notice that a frame
is not responsible for holding the environment at label Here
, since this is managed by a specific compilation environment, see env
below.
val pp_frame : Stdlib.Format.formatter -> frame -> unit
val get_frame : unit -> frame
Get the current frame, or raise a fatal error if none.
val in_frame : frame -> ('a -> 'b) -> 'a -> 'b
Execute the given closure with the specified current frame. The Lang.gamma
and Lang.pool
contexts are also set accordingly.
val mem_at_frame : frame -> Clabels.c_label -> sigma
Get the memory environment at the given label. A fresh environment is created lazily if required. The label must not be Here
.
val set_at_frame : frame -> Clabels.c_label -> sigma -> unit
Update a frame with a specific environment for the given label.
val has_at_frame : frame -> Clabels.c_label -> bool
Chek if a frame already has a specific envioronement for the given label.
val mem_frame : Clabels.c_label -> sigma
Same as mem_at_frame
but for the current 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
Full featured constructor for frames, with fresh pool and gamma.
val local : descr:string -> frame
Make a local frame reusing the current pool and gamma.
val frame : Frama_c_kernel.Cil_types.kernel_function -> frame
Make a fresh frame with the given function.
val call : ?result:M.loc -> Frama_c_kernel.Cil_types.kernel_function -> value list -> call
Create call data from the callee point of view, deriving data (gamma and pools) from the current frame. If result
is specified, the called function will stored its result at the provided location in the current frame (the callee).
Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.
val call_post : sigma -> call -> sigma Sigs.sequence -> frame
Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state and post-state.
val return : unit -> Frama_c_kernel.Cil_types.typ
Result type of the current function in the current frame.
val result : unit -> result
Result location of the current function in the current frame.
val status : unit -> Lang.F.var
Exit status for the current frame.
val guards : frame -> Lang.F.pred list
Returns the current gamma environment from the current frame.
Compilation Environment
Compilation environment for terms and predicates. Manages the current memory state and the memory state at Here
.
Remark: don't confuse the current memory state with the memory state at label Here
. The current memory state is the one we have at hand when compiling a term or a predicate. Hence, inside \at(e,L)
the current memory state when compiling e
is the one at L
.
val mk_env : ?here:sigma -> ?lvars:Frama_c_kernel.Cil_types.logic_var list -> unit -> env
Create a new environment.
Current and Here
memory points are initialized to ~here
, if provided.
The logic variables stand for formal parameters of ACSL logic function and ACSL predicates.
The current memory state. Must be propertly initialized with a specific move
before.
Move the compilation environment to the specified Here
memory state. This memory state becomes also the new current one.
val mem_at : env -> Clabels.c_label -> sigma
Returns the memory state at the requested label. Uses the local environment for Here
and the current frame otherwize.
val env_at : env -> Clabels.c_label -> env
Returns a new environment where the current memory state is moved to to the corresponding label. Suitable for compiling e
inside \at(e,L)
ACSL construct.
Compilers
val lval : env -> Frama_c_kernel.Cil_types.term_lval -> Frama_c_kernel.Cil_types.typ * M.loc
Compile a term l-value into a (typed) abstract location
val term : env -> Frama_c_kernel.Cil_types.term -> Lang.F.term
Compile a term expression.
val pred : Sigs.polarity -> env -> Frama_c_kernel.Cil_types.predicate -> Lang.F.pred
Compile a predicate. The polarity is used to generate a weaker or stronger predicate in case of unsupported feature from WP or the underlying memory model.
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
Compile a predicate call.
val region : env -> Frama_c_kernel.Cil_types.term -> region
Compile a term representing a set of memory locations into an abstract region.
val assigned_of_lval : env -> Frama_c_kernel.Cil_types.lval -> region
Computes the region assigned by a list of froms.
val assigned_of_froms : env -> Frama_c_kernel.Cil_types.from list -> region
Computes the region assigned by a list of froms.
val assigned_of_assigns : env -> Frama_c_kernel.Cil_types.assigns -> region option
Computes the region assigned by an assigns clause. None
means everyhting is assigned.
val val_of_term : env -> Frama_c_kernel.Cil_types.term -> Lang.F.term
Same as term
above but reject any set of locations.
val loc_of_term : env -> Frama_c_kernel.Cil_types.term -> loc
Same as term
above but expects a single loc or a single pointer value.
val lemma : LogicUsage.logic_lemma -> Definitions.dlemma
Compile a lemma definition.
Regions
val vars : region -> Lang.F.Vars.t
Qed variables appearing in a region expression.
val occurs : Lang.F.var -> region -> bool
Member of vars.
val check_assigns : unfold:int -> sigma -> written:region -> assignable:region -> Lang.F.pred
Check assigns inclusion. Compute a formula that checks whether written locations are either invalid (at the given memory location) or included in some assignable region. When ~unfold:n && n <> 0
, compound memory locations are expanded field-by-field and arrays, cell-by-cell (by quantification). Up to n
levels are unfolded, -1 means unlimited.