module Env:sig
..end
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.
type
localized_scope =
| |
LGlobal |
| |
LFunction of |
| |
LLocal_block of |
val new_var : loc:Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
t ->
Cil_types.kernel_function ->
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.kernel_function ->
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
.
val rtl_call_to_new_var : loc:Cil_types.location ->
?scope:Varname.scope ->
?name:string ->
t ->
Cil_types.kernel_function ->
Cil_types.term option ->
Cil_types.typ -> string -> Cil_types.exp list -> 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 : Cil_types.kernel_function -> 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.kernel_function -> 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.
before
and post
are mutually exclusive.
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
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 * localized_scope) list
All the new variables local to the visited function.
module Logic_scope:sig
..end
val annotation_kind : t -> Smart_stmt.annotation_kind
val set_annotation_kind : t -> Smart_stmt.annotation_kind -> t
val push_loop : t -> t
val set_loop_variant : ?measure:Cil_types.logic_info -> t -> Cil_types.term -> t
val add_loop_invariant : t -> Cil_types.toplevel_predicate -> t
val top_loop_variant : t -> (Cil_types.term * Cil_types.logic_info option) option
val top_loop_invariants : t -> Cil_types.toplevel_predicate list
val pop_loop : t -> t
val rte : t -> bool -> t
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
val with_rte : f:(t -> t) -> t -> bool -> t
with_rte ~f env x
executes the given closure with RTE generation set to x,
and reset RTE generation to its original value afterwards.
This function does not handle exceptions at all. The user must handle them
either directly in the f
closure or around the call to the function.
val with_rte_and_result : f:(t -> 'a * t) -> t -> bool -> 'a * t
with_rte_and_result ~f env x
executes the given closure with RTE
generation set to x, and reset RTE generation to its original value
afterwards. f
is a closure that takes an environment an returns a pair
where the first member is an arbitrary value and the second member is the
environment. The function will return the first member of the returned pair
of the closure along with the updated environment.
This function does not handle exceptions at all. The user must handle them
either directly in the f
closure or around the call to the function.
module Local_vars:sig
..end
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.
val untypable : t -> string -> 'a
Save the current context and raise Error.Typing_error
exception.
val push_contract : t -> Contract_types.contract -> t
Push a contract to the environment's stack
val top_contract : t -> Contract_types.contract * Contract_types.contract list
Return the top contract of 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
val pop_contract : t -> t
Pop the top contract of the environment's stack
val pretty : Stdlib.Format.formatter -> t -> unit