Module `Dom.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 : Frama_c_kernel.Value_types.callstack -> t -> unit

val register_state_before_stmt : 
  Frama_c_kernel.Value_types.callstack ->
  Frama_c_kernel.Cil_types.stmt ->
  t ->
  unit

val register_state_after_stmt : 
  Frama_c_kernel.Value_types.callstack ->
  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_initial_state : 
  Frama_c_kernel.Cil_types.kernel_function ->
  t Eva.Eval.or_bottom

val get_initial_state_by_callstack : 
  ?selection:Eva.Eval.callstack list ->
  Frama_c_kernel.Cil_types.kernel_function ->
  t Frama_c_kernel.Value_types.Callstack.Hashtbl.t Eva.Eval.or_top_bottom

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.Eval.callstack list ->
  after:bool ->
  Frama_c_kernel.Cil_types.stmt ->
  t Frama_c_kernel.Value_types.Callstack.Hashtbl.t Eva.Eval.or_top_bottom

val mark_as_computed : unit -> unit

val is_computed : unit -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/Dom/Store/index.html

Module `Dom.Store`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-eva.gui/Eva_gui/Gui_eval/Make/argument-1-X/Dom/Store/index.html

Module Dom.Store

Module `Dom.Store`