Module Eva_utils

module Eva_utils: sig .. end

Callstacks related types and functions

val clear_call_stack : unit -> unit

Functions dealing with call stacks.

val pop_call_stack : unit -> unit

val push_call_stack : Cil_types.kernel_function -> Cil_types.kinstr -> unit

val current_kf : unit -> Cil_types.kernel_function

The current function is the one on top of the call stack.

val call_stack : unit -> Value_types.callstack

val pp_callstack : Stdlib.Format.formatter -> unit

Prints the current callstack.

Others

val emitter : Emitter.t

val get_slevel : Kernel_function.t -> Parameters.SlevelFunction.value

val get_subdivision : Cil_types.stmt -> int

val pretty_actuals : Stdlib.Format.formatter -> (Cil_types.exp * Cvalue.V.t) list -> unit

val pretty_current_cfunction_name : Stdlib.Format.formatter -> unit

val warning_once_current : ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

val alarm_report : 'a Log.pretty_printer

Emit an alarm, either as warning or as a result, according to status associated to Self.wkey_alarm

val protect : (unit -> 'a) -> cleanup:(unit -> unit) -> 'a

protect f ~cleanup runs f. On a user interruption or a Frama-C error, if option -save is set, applies cleanup. This is used to clean up and save partial results when the analysis is aborted.

module DegenerationPoints: State_builder.Hashtbl  with type key = stmt and type data = bool

val create_new_var : string -> Cil_types.typ -> Cil_types.varinfo

Create and register a new variable inside Frama-C. The variable has its vlogic field set, meaning it is not a source variable. The freshness of the name must be ensured by the user.

val is_const_write_invalid : Cil_types.typ -> bool

Detect that the type is const, and that option -global-const is set. In this case, we forbid writing in a l-value that has this type.

val postconditions_mention_result : Cil_types.funspec -> bool

Does the post-conditions of this specification mention \result?

val conv_comp : Cil_types.binop -> Abstract_interp.Comp.t

val conv_relation : Cil_types.relation -> Abstract_interp.Comp.t

val normalize_as_cond : Cil_types.exp -> bool -> Cil_types.exp

normalize_as_cond e positive returns the expression corresponding to e != 0 when positive is true, and e == 0 otherwise. The resulting expression will always have a comparison operation at its root.

val is_value_zero : Cil_types.exp -> bool

Return true iff the argument has been created by Eva_utils.normalize_as_cond

val lval_to_exp : Cil_types.lval -> Cil_types.exp

This function is memoized to avoid creating too many expressions

val dump_garbled_mix : unit -> unit

print information on the garbled mix created during evaluation

Dependences of expressions and lvalues.

val zone_of_expr : (Cil_types.lval -> Precise_locs.precise_location) ->
       Cil_types.exp -> Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the value of an expression depends.

val indirect_zone_of_lval : (Cil_types.lval -> Precise_locs.precise_location) ->
       Cil_types.lval -> Locations.Zone.t

Given a function computing the location of lvalues, computes the memory zone on which the offset and the pointer expression (if any) of an lvalue depend.

val height_expr : Cil_types.exp -> int

Computes the height of an expression, that is the maximum number of nested operations in this expression.

val height_lval : Cil_types.lval -> int

Computes the height of an lvalue.

val skip_specifications : Cil_types.kernel_function -> bool

Should we skip the specifications of this function, according to -eva-skip-stdlib-specs