package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-wp.core/Wp/LogicSemantics/Make/index.html

Module `LogicSemantics.Make`Source

Parameters

module M : Sigs.Model

Signature

Sourcemodule M = M

Underlying memory model

Sourcetype loc = M.loc

Sourcetype nonrec value = M.loc Sigs.value

Sourcetype nonrec logic = M.loc Sigs.logic

Sourcetype nonrec region = M.loc Sigs.region

Sourcetype nonrec result = M.loc Sigs.result

Sourcetype 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.

Sourcetype frame

Sourceval pp_frame : Format.formatter -> frame -> unit

Sourceval get_frame : unit -> frame

Get the current frame, or raise a fatal error if none.

Sourceval 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.

Sourceval 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.

Sourceval set_at_frame : frame -> Clabels.c_label -> sigma -> unit

Update a frame with a specific environment for the given label.

Sourceval has_at_frame : frame -> Clabels.c_label -> bool

Chek if a frame already has a specific envioronement for the given label.

Sourceval mem_frame : Clabels.c_label -> sigma

Same as mem_at_frame but for the current frame.

Source

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

Full featured constructor for frames, with fresh pool and gamma.

Sourceval local : descr:string -> frame

Make a local frame reusing the current pool and gamma.

Sourceval frame : Frama_c_kernel.Cil_types.kernel_function -> frame

Make a fresh frame with the given function.

Sourcetype call

Internal call data.

Source

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).

Sourceval call_pre : sigma -> call -> sigma -> frame

Derive a frame from the call data suitable for compiling the called function contracts in the provided pre-state.

Sourceval 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.

Sourceval return : unit -> Frama_c_kernel.Cil_types.typ

Result type of the current function in the current frame.

Sourceval result : unit -> result

Result location of the current function in the current frame.

Sourceval status : unit -> Lang.F.var

Exit status for the current frame.

Sourceval guards : frame -> Lang.F.pred list

Returns the current gamma environment from the current frame.

Compilation Environment

Sourcetype env

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.

Source

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.

Sourceval current : env -> sigma

The current memory state. Must be propertly initialized with a specific move before.

Sourceval move_at : env -> sigma -> env

Move the compilation environment to the specified Here memory state. This memory state becomes also the new current one.

Sourceval 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.

Sourceval 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

Source

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

Sourceval term : env -> Frama_c_kernel.Cil_types.term -> Lang.F.term

Compile a term expression.

Source

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.

Source

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.

Sourceval region : env -> Frama_c_kernel.Cil_types.term -> region

Compile a term representing a set of memory locations into an abstract region.

Sourceval assigned_of_lval : env -> Frama_c_kernel.Cil_types.lval -> region

Computes the region assigned by a list of froms.

Sourceval assigned_of_froms : env -> Frama_c_kernel.Cil_types.from list -> region

Computes the region assigned by a list of froms.

Source

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.

Sourceval val_of_term : env -> Frama_c_kernel.Cil_types.term -> Lang.F.term

Same as term above but reject any set of locations.

Sourceval 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.

Sourceval lemma : LogicUsage.logic_lemma -> Definitions.dlemma

Compile a lemma definition.

Regions

Sourceval vars : region -> Lang.F.Vars.t

Qed variables appearing in a region expression.

Sourceval occurs : Lang.F.var -> region -> bool

Member of vars.

Source

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.

On This Page

Parameters
Signature

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/LogicSemantics/Make/index.html

Module LogicSemantics.MakeSource

Parameters

Signature

Frames

Compilation Environment

Compilers

Regions

Module `LogicSemantics.Make`Source