package owi

  1. Overview
  2. Docs
type 'a eval =
  1. | EVal of 'a
  2. | ETrap of Trap.t
  3. | EAssert of Smtml.Expr.t
include Choice_intf.Complete with type thread := Thread.t and type 'a run_result = ('a eval * Thread.t) Seq.t and module V := Symbolic_value
include Choice_intf.Base with module V := Symbolic_value
type 'a t
val return : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val map : 'a t -> ('a -> 'b) -> 'b t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
val trap : Trap.t -> 'a t
val let* : 'a t -> ('a -> 'b t) -> 'b t
val let+ : 'a t -> ('a -> 'b) -> 'b t
type 'a run_result = ('a eval * Thread.t) Seq.t
val assertion : Owi.Symbolic_value.vbool -> unit t
val with_thread : (Thread.t -> 'b) -> 'b t
val solver : Solver.solver t
val thread : Thread.t t
val add_pc : Owi.Symbolic_value.vbool -> unit t
val run : workers:int -> 'a t -> Thread.t -> 'a run_result
OCaml

Innovation. Community. Security.