InterpM (soteria-c.Soteria_c_lib.Abductor.Bi

module StateM : sig ... end

module SSM : sig ... end

type 'a t = ('a, Error.with_trace, Bi_state.syn list) SSM.Result.t

val map : ('a, 'b, 'c) SSM.Result.t -> ('a -> 'd) -> ('d, 'b, 'c) SSM.Result.t

val bind : 
  ('a, 'b, 'c) SSM.Result.t ->
  ('a -> ('d, 'b, 'c) SSM.Result.t) ->
  ('d, 'b, 'c) SSM.Result.t

module Syntax : sig ... end

val ok : 'a -> 'a t

val not_impl : string -> 'a t

val get_store : unit -> Store.t t

val fold_list : 'a list -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t

val iter_list : 'a list -> f:('a -> unit t) -> unit t

val map_list : 
  'a list ->
  f:('a -> ('b, Error.with_trace, Bi_state.syn list) SSM.Result.t) ->
  ('b list, Error.with_trace, Bi_state.syn list) SSM.Result.t

val map_store : 
  (SSM.st -> SSM.st) ->
  (unit, 'a, 'b) Soteria.Symex.Compo_res.t SSM.t

val lift_state_op : 'a SSM.Symex.t -> 'a SSM.t

val lift_symex : 'a Csymex.t -> 'a t

val lift_symex_res : 
  ('a, Error.with_trace, Bi_state.syn list) Csymex.Result.t ->
  'a t

val error : Error.t -> 'a t

val of_opt_not_impl : msg:string -> 'a option -> 'a t

val assert_or_error : SSM.Value.sbool SSM.Value.t -> Error.t -> unit t

val with_loc : loc:Cerb_location.t -> 'a t -> 'a t

val with_extra_call_trace : loc:Cerb_location.t -> msg:string -> 'a t -> 'a t

val run : 
  store:Store.t ->
  state:StateM.st ->
  'a t ->
  ((('a, Error.with_trace, Bi_state.syn list) Soteria.Symex.Compo_res.t
    * Store.t)
   * StateM.st)
    StateM.Symex.t

module IState : sig ... end

module IStore : sig ... end