package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Make.Equality

include Soteria.Soteria_std.Reversible.Mutable
type t
val init : unit -> t

Create a new reversible state initialized with the default value.

val backtrack_n : t -> int -> unit

Remove the last n checkpoints from state.

val save : t -> unit

Save the current state as a new checkpoint.

val reset : t -> unit

Clear all checkpoints and reset to the default value.

val simplify : t -> Svalue.t -> Svalue.t

Simplifies a constraints using the current knowledge base, without updating it.

val add_constraint : t -> Svalue.t -> Svalue.t * Soteria.Symex.Var.Set.t

Adds a constraint to the current analysis, updating the currently tracked data.

Filters the given iterator of symbolic values, keeping only those relevant to the given variable according to the analysis.

Encode all the information relevant to the given variables and conjuncts them with the given accumulator.