Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_utils

Others

Emitter of alarms and logical statuses evaluated by the analysis.

val export_emitter : Frama_c_kernel.Emitter.t

Emitter of code annotations stating the properties inferred by an analysis, intended for other plug-ins. Used by the Export module.

val get_subdivision : Frama_c_kernel.Cil_types.stmt -> int
val pretty_actuals : Stdlib.Format.formatter -> (Eva_ast.exp * Frama_c_kernel.Cvalue.V.t) list -> unit
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.

val create_new_var : ?alignas:int -> string -> Frama_c_kernel.Cil_types.typ -> Frama_c_kernel.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 : Frama_c_kernel.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.

Returns the varinfo returned by the given function. Returns None if the function returns void or has no return statement.

val postconditions_mention_result : Frama_c_kernel.Cil_types.funspec -> bool

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

This function is memoized to avoid creating too many expressions

val height_expr : Frama_c_kernel.Cil_types.exp -> int

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

val height_lval : Frama_c_kernel.Cil_types.lval -> int

Computes the height of an lvalue.

val skip_specifications : Frama_c_kernel.Cil_types.kernel_function -> bool

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