Module Ctree_block.MemVal

module S_bool = Soteria_c_lib.Typed.Bool
module S_bounded_int : sig ... end
val pp_init : Stdlib.Format.formatter -> ('a Typed.t * Cerb_frontend.Ctype.ctype) -> unit
type qty =
  1. | Totally
  2. | Partially
val pp_qty : Ppx_deriving_runtime.Format.formatter -> qty -> Ppx_deriving_runtime.unit
val show_qty : qty -> Ppx_deriving_runtime.string
type t =
  1. | Init of Soteria_c_lib.Typed.T.cval Typed.t * Ctype.ctype
  2. | Zeros
  3. | Uninit of qty
  4. | Any
  5. | Lazy
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val any_of_type : Ctype.ctype -> Cerb_location.t -> ((Soteria_c_lib.Typed.T.cval Typed.t * Ctype.ctype) * Cerb_location.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t
val merge : left:t -> right:t -> t
val split : at:'a -> t -> ((t, 'b) TB.Split_tree.t * (t, 'c) TB.Split_tree.t) Csymex.t
val decode : ty:Ctype.ctype -> t -> (Soteria_c_lib.Typed.T.cval Typed.t, [> `UninitializedMemoryAccess ], 'fix) Csymex.Result.t
type syn =
  1. | SInit of Soteria_c_lib.Typed.Expr.t * Ctype.ctype
  2. | SUninit
  3. | SZeros
  4. | SAny
val pp_syn : Ppx_deriving_runtime.Format.formatter -> syn -> Ppx_deriving_runtime.unit
val show_syn : syn -> Ppx_deriving_runtime.string
val ins_outs : syn -> 'a list * Soteria_c_lib.Typed.Expr.t list
val to_syn : t -> syn Soteria.Soteria_std.Seq.t option
val mk_fix_typed : Soteria_c_lib.Layout.CF.Ctype.ctype -> unit -> Cerb_location.t -> (syn list * Cerb_location.t) Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t
val mk_fix_any : unit -> t list
val not_owned : tree -> tree
val owned : tree -> t -> tree
val consume : syn -> tree -> (tree, syn list) Soteria_c_lib.Csymex.Consumer.t
val assert_exclusively_owned : 'a -> (unit, 'b, 'c) Csymex.Result.t