IState (soteria-c.Soteria_c_lib.Abductor.Bi

val load : 
  [< Soteria_c_lib.Typed.T.sptr ] Typed.t ->
  Soteria_c_lib.Ctree_block.Ctype.ctype ->
  (Aggregate_val.t, Error.with_trace, Bi_state.syn list)
    Soteria.Symex.Compo_res.t
    SSM.t

val store : 
  Soteria_c_lib.Typed.T.sptr Typed.t ->
  Soteria_c_lib.Ctree_block.Ctype.ctype ->
  Aggregate_val.t ->
  (unit, Error.with_trace, Bi_state.syn list) Soteria.Symex.Compo_res.t SSM.t

val alloc : 
  ?zeroed:bool ->
  Soteria_c_lib.Typed.T.sint Typed.t ->
  ([> Soteria_c_lib.Typed.T.sptr ] Typed.t,
    Error.with_trace,
    Bi_state.syn list)
    Soteria.Symex.Compo_res.t
    SSM.t

val alloc_ty : 
  Soteria_c_lib.Ctree_block.Ctype.ctype ->
  ([> Soteria_c_lib.Typed.T.sptr ] Typed.t,
    Error.with_trace,
    Bi_state.syn list)
    Soteria.Symex.Compo_res.t
    SSM.t

val free : 
  [< Soteria_c_lib.Typed.T.sptr ] Typed.t ->
  (unit, Error.with_trace, Bi_state.syn list) Soteria.Symex.Compo_res.t SSM.t

val get_global : 
  Cerb_frontend.Symbol.sym ->
  ([> Soteria_c_lib.Typed.T.sptr ] Typed.t Aggregate_val.agv, 'a, 'b)
    Soteria.Symex.Compo_res.t
    SSM.t