package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Current annotation kind
Loop annotations
RTEs
Context for error handling
Current environment kinstr
Contracts
Utilities

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.0-beta-Cobalt.tar.gz

sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

doc/frama-c-e-acsl.core/E_ACSL/Env/index.html

Module `E_ACSL.Env`

val gmp_clear_ref : 
  (Frama_c_kernel.Cil_types.location ->
    Frama_c_kernel.Cil_types.exp ->
    Frama_c_kernel.Cil_types.stmt)
    ref

Environments.

Environments handle all the new C constructs (variables, statements and annotations.

type t

val empty : t

val has_no_new_stmt : t -> bool

Assume that a local context has been previously pushed.

returns
true iff the given env does not contain any new statement.

type localized_scope =

| LGlobal
| LFunction of Frama_c_kernel.Cil_types.kernel_function
| LLocal_block of Frama_c_kernel.Cil_types.kernel_function

val new_var : 
  loc:Frama_c_kernel.Cil_types.location ->
  ?scope:Varname.scope ->
  ?name:string ->
  t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.term option ->
  Frama_c_kernel.Cil_types.typ ->
  (Frama_c_kernel.Cil_types.varinfo ->
    Frama_c_kernel.Cil_types.exp ->
    Frama_c_kernel.Cil_types.stmt list) ->
  Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.exp * t

new_var env t ty mk_stmts extends env with a fresh variable of type ty corresponding to t. scope is the scope of the new variable (default is Block).

returns
this variable as both a C variable and a C expression already initialized by applying it to mk_stmts.

val rtl_call_to_new_var : 
  loc:Frama_c_kernel.Cil_types.location ->
  ?scope:Varname.scope ->
  ?name:string ->
  t ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.term option ->
  Frama_c_kernel.Cil_types.typ ->
  string ->
  Frama_c_kernel.Cil_types.exp list ->
  Frama_c_kernel.Cil_types.exp * t

rtl_call_to_new_var env t ty name args Same as new_var but initialize the variable with a call to the RTL function name with the given args.

module Logic_binding : sig ... end

val add_assert : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.predicate ->
  unit

add_assert env s p associates the assertion p to the statement s in the environment env.

val add_stmt : ?post:bool -> t -> Frama_c_kernel.Cil_types.stmt -> t

add_stmt env s extends env with the new statement s. post indicates that stmt should be added after the target statement.

val extend_stmt_in_place : 
  t ->
  Frama_c_kernel.Cil_types.stmt ->
  label:Frama_c_kernel.Cil_types.logic_label ->
  Frama_c_kernel.Cil_types.block ->
  t

extend_stmt_in_place env stmt ~label b modifies stmt in place in order to add the given block. If label is Here or Post, then this block is guaranteed to be at the first place of the resulting stmt whatever modification will be done by the visitor later.

val push : t -> t

Push a new local context in the environment

type where =

| Before
| Middle
| After

val pop_and_get : 
  ?split:bool ->
  t ->
  Frama_c_kernel.Cil_types.stmt ->
  global_clear:bool ->
  where ->
  Frama_c_kernel.Cil_types.block * t

Pop the last local context and get back the corresponding new block containing the given stmt at the given place (Before is before the code corresponding to annotations, After is after this code and Middle is between the stmt corresponding to annotations and the ones for freeing the memory. When where is After, set split to true in order to generate one block which contains exactly 2 stmt: one for stmt and one sub-block for the generated stmts.

val pop : t -> t

Pop the last local context (ignore the corresponding new block if any

val transfer : from:t -> t -> t

Pop the last local context of from and push it into the other env.

val get_generated_variables : 
  t ->
  (Frama_c_kernel.Cil_types.varinfo * localized_scope) list

All the new variables local to the visited function.

module Logic_scope : sig ... end

Current annotation kind

val annotation_kind : t -> Analyses_types.annotation_kind

val set_annotation_kind : t -> Analyses_types.annotation_kind -> t

Loop annotations

val push_loop : t -> t

val set_loop_variant : 
  ?measure:Frama_c_kernel.Cil_types.logic_info ->
  t ->
  Frama_c_kernel.Cil_types.term ->
  t

val add_loop_invariant : t -> Frama_c_kernel.Cil_types.toplevel_predicate -> t

val top_loop_variant : 
  t ->
  (Frama_c_kernel.Cil_types.term * Frama_c_kernel.Cil_types.logic_info option)
    option

val top_loop_invariants : t -> Frama_c_kernel.Cil_types.toplevel_predicate list

val pop_loop : t -> t

RTEs

val set_rte : t -> bool -> t

set_rte env x sets RTE generation to x for the given environment

val generate_rte : t -> bool

Returns the current value of RTE generation for the given environment

module Logic_env : sig ... end

Context for error handling

module Context : sig ... end

val handle_error : (t -> t) -> t -> t

Run the closure with the given environment and handle potential errors. Restore the globals of the environment to the last time Env.Context.save was called and return it in case of errors.

val handle_error_with_args : ((t * 'a) -> t * 'a) -> (t * 'a) -> t * 'a

Run the closure with the given environment and arguments and handle potential errors. Restore the globals of the environment to the last time Env.Context.save was called and return it in case of errors.

val not_yet : t -> string -> 'a

Save the current context and raise Error.Not_yet exception.

Current environment kinstr

val set_kinstr : t -> Frama_c_kernel.Cil_types.kinstr -> t

val get_kinstr : t -> Frama_c_kernel.Cil_types.kinstr

Contracts

val push_contract : t -> Contract_types.contract -> t

Push a contract to the environment's stack

val pop_and_get_contract : t -> Contract_types.contract * t

Pop and return the top contract of the environment's stack

Utilities

val with_params : 
  ?rte:bool ->
  ?kinstr:Frama_c_kernel.Cil_types.kinstr ->
  f:(t -> t) ->
  t ->
  t

with_params ~rte ~kinstr ~f env executes the given closure with the given environment after having set RTE generation to rte and current kinstr to kinstr. f is a closure that takes an environment and returns an environment. The environment returned by the closure is updated to restore the RTE generation and kinstr attributes to the values of the original environment, then is returned.

val with_params_and_result : 
  ?rte:bool ->
  ?kinstr:Frama_c_kernel.Cil_types.kinstr ->
  f:(t -> 'a * t) ->
  t ->
  'a * t

with_params_and_result ~rte ~kinstr ~f env executes the given closure with the given environment after having set RTE generation to rte and current kinstr to kinstr. f is a closure that takes an environment and returns a pair where the first member is an arbitrary value and the second member is the environment. The environment returned by the closure is updated to restore the RTE generation and kinstr attributes to the values of the original environment, then the function returns the arbitrary value returned by the closure along with the updated environment.

val pretty : Format.formatter -> t -> unit