package soteria

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

Module Symex.Make_core

Parameters

Signature

module Solver : sig ... end
module Solver_pool : sig ... end
module Fuel : sig ... end
module Value = Solver.Value
include module type of struct include MONAD end
val return : 'a -> ('a -> unit) -> unit
val bind : ('a -> ('b -> unit) -> unit) -> (('a -> unit) -> unit) -> ('b -> unit) -> unit
val map : ('a -> 'b) -> (('a -> unit) -> unit) -> ('b -> unit) -> unit
val fold : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> init:'a -> f:('a -> 'elem -> ('a -> unit) -> unit) -> ('a -> unit) -> unit
val fold_list : 'elem list -> init:'a -> f:('a -> 'elem -> ('a -> unit) -> unit) -> ('a -> unit) -> unit
val fold_iter : 'elem Iter.t -> init:'a -> f:('a -> 'elem -> ('a -> unit) -> unit) -> ('a -> unit) -> unit
val iter : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> (unit -> unit) -> unit) -> (unit -> unit) -> unit
val iter_list : 'elem list -> f:('elem -> (unit -> unit) -> unit) -> (unit -> unit) -> unit
val iter_iter : 'elem Iter.t -> f:('elem -> (unit -> unit) -> unit) -> (unit -> unit) -> unit
val map_m : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> ('a -> unit) -> unit) -> ('a list -> unit) -> unit
val map_list : 'elem list -> f:('elem -> ('a -> unit) -> unit) -> ('a list -> unit) -> unit
val map_iter : 'elem Iter.t -> f:('elem -> ('a -> unit) -> unit) -> ('a list -> unit) -> unit
module Syntax = MONAD.Syntax
module Flamegraph : sig ... end
module Give_up : sig ... end
type 'a t = 'a Soteria_std.Iter.t
type lfail = [
  1. | `Lfail of Value.sbool Value.t
]
type cons_fail = [
  1. | lfail
  2. | `Missing_subst of Var.t
]
val show_cons_fail : cons_fail -> Ppx_deriving_runtime.string
module Symex_state : sig ... end
val signal_unexplored_branch : [ `Branch | `Step ] -> unit
val consume_fuel_steps : int -> (unit -> unit) -> unit
val log_solver_state : level:Soteria__Logs.Level.t -> unit -> unit
val simplified_bool : 'a Value.t -> 'a Value.t * bool option

Solver.simplify throws an effect to ask the solver for simplification. When the value is already a concrete boolean literal, we can skip the effect dispatch entirely.

simplified_bool returns the simplified value together with an its to_bool.

val assume : Sol.Value.sbool Value.t list -> (unit -> unit) -> unit
val assert_raw : Value.sbool Value.t -> bool

Same as assert_, but not captured within the monad. Not to be exposed to the user, because without proper care, this could have unwanted side-effects at the wrong time.

val assert_ : Value.sbool Value.t -> (bool -> 'a) -> 'a

Assert is if%sat (not value) then error else ok. In UX, assert only returns false if (not value) is satisfiable. In OX, assert only returns true if (not value) is unsatisfiable.

val nondet_UNSAFE : 'a Value.ty -> 'a Value.t
val nondet : 'a Value.ty -> ('a Value.t -> 'b) -> 'b
val simplify : 'a Sol.Value.t -> ('a Sol.Value.t -> 'b) -> 'b
val fresh_var : 'a Sol.Value.ty -> (Symex.Var.t -> 'b) -> 'b
val branch_on : ?left_branch_name:??? -> ?right_branch_name:??? -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val if_sure : ?left_branch_name:??? -> ?right_branch_name:??? -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val branch_on_take_one_ux : ?left_branch_name:??? -> ?right_branch_name:??? -> Value.sbool Value.t -> then_:(unit -> ('a -> unit) -> unit) -> else_:(unit -> ('a -> unit) -> unit) -> 'a t
val branch_on_take_one : ?left_branch_name:??? -> ?right_branch_name:??? -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> ('a -> unit) -> unit
val branches : (unit -> 'a t) list -> 'a t
val vanish : unit -> 'a -> unit
val give_up : string -> 'a -> unit
val with_frame : string -> (unit -> 'a MONAD.t) -> 'a MONAD.t