Symex (soteria.Soteria.Symex)

module Approx : sig ... end

module Compo_res : sig ... end

This module defines a three-way result type for compositional symbolic execution. Unlike standard Result.t which has two cases (Ok/Error), this type adds a third case Missing for bi-abduction scenarios where anti-frame inference is needed, or more generally to represent incompletenesses in the engine.

module Fuel_gauge : sig ... end

module Solver : sig ... end

module Solver_result : sig ... end

module Value : sig ... end

This module defines the minimal interface that symbolic values must implement to be used in Soteria's symbolic execution engine.

module Var : sig ... end

exception Tool_bug of string

exception Gave_up of string

val tool_bug : string -> 'a

module Or_gave_up : sig ... end

module type Symex_syntax_S = sig ... end

module type Core = sig ... end

module type Base = sig ... end

module type S = sig ... end

module StatKeys : sig ... end

Keys for statistics used in Soteria's symex engine. These are exposed so clients can query statistics if needed; the type with which they are logged is also documented.

module Make_core (Sol : Solver.Mutable_incremental) : sig ... end

module Base_extension (Core : Core) : sig ... end

module Make
  (Sol : Solver.Mutable_incremental) : 
  S with module Value = Sol.Value