Bi_state (soteria-c.Soteria_c_lib.Bi

type t = State.t option * State.syn list

include State_intf.S with type t := t with type syn = State.syn

include Soteria.Sym_states.Base.M(Csymex).S
  with type syn = State_intf.syn
  with type t := t
  with type syn = State.syn

val pp : 
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

module SM : 
  Soteria.Sym_states.State_monad.S
    with module Symex = Csymex
     and module Value = Csymex.Value
     and type st = t option

type syn = State.syn

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

val show_syn : syn -> Ppx_deriving_runtime.string

val to_syn : t -> syn list

val ins_outs : syn -> Csymex.Value.Expr.t list * Csymex.Value.Expr.t list

val produce : syn -> t option -> t option Csymex.Producer.t

val consume : syn -> t option -> (t option, syn list) Csymex.Consumer.t

type 'a res := ('a, Error.with_trace, syn list) SM.Result.t

val pp_pretty : ignore_freed:bool -> Stdlib.Format.formatter -> t -> unit

Prettier but expensive printing.

val empty : t option

val load : 
  [< Soteria_c_lib.Typed.T.sptr ] Typed.t ->
  Soteria_c_lib.Ctree_block.Ctype.ctype ->
  Soteria_c_lib.State_intf.Agv.t res

val store : 
  Soteria_c_lib.Typed.T.sptr Typed.t ->
  Soteria_c_lib.Ctree_block.Ctype.ctype ->
  Soteria_c_lib.State_intf.Agv.t ->
  unit res

val zero_range : 
  [< Soteria_c_lib.Typed.T.sptr ] Typed.t ->
  Soteria_c_lib.Typed.T.sint Typed.t ->
  unit res

val alloc : 
  ?zeroed:bool ->
  Soteria_c_lib.Typed.T.sint Typed.t ->
  [> Soteria_c_lib.Typed.T.sptr ] Typed.t res

val alloc_ty : 
  Soteria_c_lib.Ctree_block.Ctype.ctype ->
  [> Soteria_c_lib.Typed.T.sptr ] Typed.t res

val free : [< Soteria_c_lib.Typed.T.sptr ] Typed.t -> unit res

val get_global : 
  Cerb_frontend.Symbol.sym ->
  t option ->
  ([> Soteria_c_lib.Typed.T.sptr ] Typed.t * t option) Csymex.t

val copy_nonoverlapping : 
  dst:[< Soteria_c_lib.Typed.T.sptr ] Typed.t ->
  src:[< Soteria_c_lib.Typed.T.sptr ] Typed.t ->
  size:Soteria_c_lib.Typed.T.sint Typed.t ->
  unit res

val produce_aggregate : 
  Soteria_c_lib.Typed.Expr.t ->
  Cerb_frontend.Ctype.ctype ->
  Aggregate_val.syn ->
  t option ->
  t option Soteria_c_lib.Csymex.Producer.t

val to_spec : t option -> pre:syn list * post:syn list