package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct