Module Soteria_c_lib.Csymex

module SYMEX : sig ... end
module Concrete_alloc_id : sig ... end
module CSYMEX : sig ... end
include module type of struct include CSYMEX end
type st = Cerb_location.t
module Symex = CSYMEX.Symex
type 'a t = Cerb_location.t -> ('a * Cerb_location.t) SYMEX.t
val get_state : unit -> st t
val set_state : st -> unit t
val map_state : (st -> st) -> unit t
val run_with_state : state:st -> 'a t -> ('a * st) Symex.t
val with_state : state:st -> 'a t -> 'a t
val lift : 'a Symex.t -> 'a t
module Value = CSYMEX.Value
val return : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val map : 'a t -> ('a -> 'b) -> 'b t
type lfail = [
  1. | `Lfail of Value.sbool Value.t
]
val pp_lfail : Ppx_deriving_runtime.Format.formatter -> lfail -> Ppx_deriving_runtime.unit
val show_lfail : lfail -> Ppx_deriving_runtime.string
type cons_fail = [
  1. | `Lfail of Value.sbool Value.t
  2. | `Missing_subst of Soteria.Symex.Var.t
]
val pp_cons_fail : Ppx_deriving_runtime.Format.formatter -> cons_fail -> Ppx_deriving_runtime.unit
val show_cons_fail : cons_fail -> Ppx_deriving_runtime.string
val assume : Value.sbool Value.t list -> unit t
val vanish : unit -> 'a t
val assert_ : Value.sbool Value.t -> bool t
val nondet_UNSAFE : 'a Value.ty -> 'a Value.t
val nondet : 'a Value.ty -> 'a Value.t t
val simplify : 'a Value.t -> 'a Value.t t
val fresh_var : 'a Value.ty -> Soteria.Symex.Var.t t
val branch_on : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val if_sure : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val branch_on_take_one : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val give_up : string -> 'a t
val branches : (unit -> 'a t) list -> 'a t
val consume_fuel_steps : int -> unit t
val assert_or_error : Value.sbool Value.t -> 'err -> (unit, 'err, 'f) Soteria.Symex.Compo_res.t t
val some_or_give_up : string -> 'a option -> 'a t
val all : ('a -> 'b t) -> 'a list -> 'b list t
val fold_list : 'a list -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val fold_iter : 'a Soteria.Soteria_std.Iter.t -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val fold_seq : 'a Soteria.Soteria_std.Seq.t -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val iter_list : 'a list -> f:('a -> unit t) -> unit t
val iter_iter : 'a Soteria.Soteria_std.Iter.t -> f:('a -> unit t) -> unit t
val map_list : 'a list -> f:('a -> 'b t) -> 'b list t
module Producer = CSYMEX.Producer
module Consumer = CSYMEX.Consumer
module Syntax = CSYMEX.Syntax
include module type of struct include Soteria.Soteria_std.Syntaxes.FunctionWrap end
val (let@) : ('a -> 'b) -> 'a -> 'b
val (let@@) : ('a -> 'b) -> (unit -> 'a) -> 'b
module StatKeys : sig ... end
val fresh_alloc_id : unit -> [> Soteria__Bv_values__Typed.T.sloc ] Value.t t
val check_nonzero : Soteria_c_lib.Typed.T.sint Typed.t -> ([> Soteria_c_lib.Typed.T.nonzero ] Typed.t, [> `NonZeroIsZero ], 'fix) CSYMEX.Result.t
val get_loc : unit -> st t
val with_loc : loc:Cerb_location.t -> 'a t -> 'a t
val not_impl : string -> 'a CSYMEX.t
val of_opt : 'a option -> 'a t
val of_opt_not_impl : msg:string -> 'a option -> 'a t
val run : ?fuel:Soteria.Symex.Fuel_gauge.t -> mode:Soteria.Symex.Approx.t -> 'a t -> ('a * SYMEX.Value.sbool SYMEX.Value.t list) list
val run_needs_stats : ?fuel:Soteria.Symex.Fuel_gauge.t -> mode:Soteria.Symex.Approx.t -> 'a t -> ('a * SYMEX.Value.sbool SYMEX.Value.t list) list
module Result : sig ... end
module Freeable (I : sig ... end) : sig ... end
module Pmap_direct_access (Key : sig ... end) (Codom : Soteria.Sym_states.Base.M(CSYMEX).S) : sig ... end
module Pmap (Key : sig ... end) (Codom : Soteria.Sym_states.Base.M(CSYMEX).S) : sig ... end
module Tree_block (MemVal : sig ... end) : sig ... end
module Bi (B : Soteria.Sym_states.Base.M(CSYMEX).S) : sig ... end
module Pure_fun (C : sig ... end) : sig ... end