Frama-C:
Plug-ins:
Libraries:

Frama-C API - Store

Storage of the states computed by the analysis. Automatically built by Domain_builder.Complete.

val register_global_state : bool -> t Eva.Eval.or_bottom -> unit

Called once at the analysis beginning for the entry state of the main function. The boolean indicates whether the states of this domain must be saved during the analysis, according to options -eva-no-results. If it is false, register functions do nothing, and get functions return Top.

val register_initial_state : Eva.Callstack.t -> Frama_c_kernel.Cil_types.kernel_function -> t -> unit
val register_state_before_stmt : Eva.Callstack.t -> Frama_c_kernel.Cil_types.stmt -> t -> unit
val register_state_after_stmt : Eva.Callstack.t -> Frama_c_kernel.Cil_types.stmt -> t -> unit
val get_global_state : unit -> t Eva.Eval.or_bottom

Allows accessing the states inferred by an Eva analysis after it has been computed with the domain enabled.

val get_stmt_state : after:bool -> Frama_c_kernel.Cil_types.stmt -> t Eva.Eval.or_bottom
val get_stmt_state_by_callstack : ?selection:Eva.Callstack.t list -> after:bool -> Frama_c_kernel.Cil_types.stmt -> t Eva.Callstack.Hashtbl.t Eva.Eval.or_top_bottom
val mark_as_computed : unit -> unit
val is_computed : unit -> bool