Freeable_ctree_block (soteria-c.Soteria_c_lib.Block.Freeable_ctree

type t

val show : t -> Ppx_deriving_runtime.string

val pp' : 
  ?inner:
    (Stdlib.Format.formatter -> Ctree_block.t -> Ppx_deriving_runtime.unit) ->
  Stdlib.Format.formatter ->
  Ctree_block.t Soteria__Sym_states__Freeable.freeable ->
  Ppx_deriving_runtime.unit

val pp : 
  Stdlib.Format.formatter ->
  Ctree_block.t Soteria__Sym_states__Freeable.freeable ->
  Ppx_deriving_runtime.unit

type syn

val pp_syn : 
  Ppx_deriving_runtime.Format.formatter ->
  syn ->
  Ppx_deriving_runtime.unit

val show_syn : syn -> Ppx_deriving_runtime.string

module SM : sig ... end

val lift_fix : 'a -> 'a Soteria__Sym_states__Freeable.freeable

val lift_fix_r : 
  ('a, 'b, 'c list) Soteria.Symex.Compo_res.t ->
  ('a, 'b, 'c Soteria__Sym_states__Freeable.freeable list)
    Soteria.Symex.Compo_res.t

val lift_fix_c : 
  ('a, 'b list) Soteria_c_lib__Csymex.CSYMEX.Consumer.t ->
  ('a, 'b Soteria__Sym_states__Freeable.freeable list)
    Soteria_c_lib__Csymex.CSYMEX.Consumer.t

val to_syn : 
  Ctree_block.t Soteria__Sym_states__Freeable.freeable ->
  Ctree_block.syn Soteria__Sym_states__Freeable.freeable list

val ins_outs : 
  Ctree_block.syn Soteria__Sym_states__Freeable.freeable ->
  Soteria.Bv_values.Bv_solver.Z3_solver.Value.Expr.t list
  * Soteria.Bv_values.Bv_solver.Z3_solver.Value.Expr.t list

val unwrap_alive : 
  unit ->
  (Ctree_block.t option, [> `UseAfterFree ], 'a) Soteria.Symex.Compo_res.t SM.t

val wrap : 
  ('b, [> `UseAfterFree ] as 'a, Ctree_block.syn list) Ctree_block.SM.Result.t ->
  ('b, 'a, syn list) SM.Result.t

val free : unit -> (unit, [> `UseAfterFree ], syn list) SM.Result.t

val produce : 
  syn ->
  Ctree_block.t Soteria__Sym_states__Freeable.freeable option ->
  SM.st SM.Symex.Producer.t

val consume : syn -> SM.st -> (SM.st, syn list) SM.Symex.Consumer.t