Frama-C:
Plug-ins:
Libraries:

Frama-C API - Store

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

val set_state : ?callstack:Callstack.t -> Eva__.Domain_store.control_point -> t -> unit

Registers the state computed at a control point:

  • for the given callstack if provided;
  • for any callstack otherwise.
val get_state : ?callstack:Callstack.t -> Eva__.Domain_store.control_point -> t Eval.or_top_bottom

Returns:

  • `Top if no analysis has started or if states are not stored.
  • or the state set by the last call to set_state with the same arguments.
  • or `Bottom if no such call has been made.
val callstacks : Eva__.Domain_store.control_point -> Callstack.t list Eval.or_top

Returns all callstacks from previous calls to set_state for the given control point.

val is_computed : unit -> bool

Are states of this domain saved?