module Env:sig
..end
Environments handle all the new C constructs (variables, statements and annotations.
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
type
localized_scope =
| |
LGlobal |
| |
LFunction of |
| |
LLocal_block of |
val new_var : loc:Cil_types.location ->
?scope:Varname.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
).mk_stmts
.val new_var_and_mpz_init : loc:Cil_types.location ->
?scope:Varname.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
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 : ?post: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 one is included before. This is to
say that any labels attached to before
are moved to stmt
. post
indicates that stmt
should be added after the target statement.val extend_stmt_in_place : t ->
Cil_types.stmt -> label:Cil_types.logic_label -> 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
type
where =
| |
Before |
| |
Middle |
| |
After |
val pop_and_get : ?split:bool ->
t ->
Cil_types.stmt -> global_clear:bool -> where -> Cil_types.block * t
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
val transfer : from:t -> t -> t
from
and push it into the other env.val get_generated_variables : t -> (Cil_types.varinfo * localized_scope) list
val get_visitor : t -> Visitor.generic_frama_c_visitor
val get_behavior : t -> Visitor_behavior.t
val current_kf : t -> Cil_types.kernel_function option
module Logic_scope:sig
..end
val set_current_kf : t -> Cil_types.kernel_function -> unit
val annotation_kind : t -> Misc.annotation_kind
val set_annotation_kind : t -> Misc.annotation_kind -> t
val push_loop : t -> t
val add_loop_invariant : t -> Cil_types.predicate -> t
val pop_loop : t -> Cil_types.predicate list * t
val rte : t -> bool -> t
val generate_rte : t -> bool
module Context:sig
..end
val pretty : Format.formatter -> t -> unit