Module Symex.Consumer

type ('a, 'fix) t = ('a, 'fix) Soteria_c_lib.Csymex.Consumer.t
val apply_subst : ((Value.Expr.t -> 'a Value.t) -> 'syn -> 'sem) -> 'syn -> ('sem, 'fix) t
val assert_pure : Value.sbool Value.t -> (unit, 'fix) t
val consume_pure : Value.Expr.t -> (unit, 'fix) t
val learn_eq : Value.Expr.t -> 'a Value.t -> (unit, 'fix) t
val expose_subst : unit -> (Value.Expr.Subst.t, 'fix) t
val lift_res : ('a, cons_fail, 'fix) Result.t -> ('a, 'fix) t
val lift : 'a t -> ('a, 'fix) t
val branches : (unit -> ('a, 'fix) t) list -> ('a, 'fix) t
val ok : 'a -> ('a, 'fix) t
val lfail : Value.sbool Value.t -> ('a, 'fix) t
val miss : 'fix list -> ('a, 'fix) t
val miss_no_fix : reason:string -> unit -> ('a, 'fix) t
val map : ('a, 'fix) t -> ('a -> 'b) -> ('b, 'fix) t
val map_missing : ('a, 'fix) t -> ('fix -> 'g) -> ('a, 'g) t
val bind : ('a, 'fix) t -> ('a -> ('b, 'fix) t) -> ('b, 'fix) t
val fold_list : 'a list -> init:'b -> f:('b -> 'a -> ('b, 'fix) t) -> ('b, 'fix) t
val iter_list : 'a list -> f:('a -> (unit, 'fix) t) -> (unit, 'fix) t
val bind_res : ('a, 'fix) t -> (('a, cons_fail, 'fix) Soteria.Symex.Compo_res.t -> ('b, 'fix2) t) -> ('b, 'fix2) t
val run : subst:Value.Expr.Subst.t -> ('a, 'fix) t -> ('a * Value.Expr.Subst.t, cons_fail, 'fix) Result.t
module Syntax : sig ... end