Module Env

module Env: sig .. end

Environments.

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

Loop invariants

Environments.

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

type t

val dummy : t

val empty : Visitor.frama_c_visitor -> 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 scope =

`\|`	`Global`
`\|`	`Function`
`\|`	`Local_block`

val new_var : loc:Cil_types.location ->
       ?init:bool ->
       ?scope:scope ->
       ?name:string ->
       t ->
       Cil_types.term option ->
       Cil_types.typ ->
       (Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
       Cil_types.varinfo * 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). init indicates if the initial env must be used.
Returns this variable as both a C variable and a C expression already initialized by applying it to mk_stmts.

val new_var_and_mpz_init : loc:Cil_types.location ->
       ?init:bool ->
       ?scope:scope ->
       ?name:string ->
       t ->
       Cil_types.term option ->
       (Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
       Cil_types.varinfo * Cil_types.exp * t

Same as new_var, but dedicated to mpz_t variables initialized by Mpz.init.

module Logic_binding: sig .. end

val add_assert : t -> Cil_types.stmt -> Cil_types.predicate -> unit

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

val add_stmt : ?init:bool -> ?before:Cil_types.stmt -> t -> Cil_types.stmt -> t

add_stmt env s extends env with the new statement s. before may define which stmt the new is included before.

val extend_stmt_in_place : t -> Cil_types.stmt -> pre:bool -> Cil_types.block -> t

extend_stmt_in_place env stmt ~pre b modifies stmt in place in order to add the given block. If pre is true, 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 ->
       Cil_types.stmt -> global_clear:bool -> where -> 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 -> (Cil_types.varinfo * scope) list

All the new variables local to the visited function. The boolean indicates whether the varinfo must be added to the outermost function block.

val get_visitor : t -> Visitor.generic_frama_c_visitor

val get_behavior : t -> Cil.visitor_behavior

val current_kf : t -> Cil_types.kernel_function option

Kernel function currently visited in the new project.

Current annotation kind

val annotation_kind : t -> Misc.annotation_kind

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

Loop invariants

val push_loop : t -> t

val add_loop_invariant : t -> Cil_types.predicate -> t

val pop_loop : t -> Cil_types.predicate list * t

RTEs

val rte : t -> bool -> t

val generate_rte : t -> bool

Context for error handling

module Context: sig .. end

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