Module MonadicSVal.SVArray

type t =
  1. | Arr of Gillian.Gil_syntax.Expr.t
    (*

    the parameter should be a list representing a *NON-EMPTY* list

    *)
  2. | AllUndef
  3. | AllZeros
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val _ : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val reduce : t -> t Monadic.Delayed.t
val pp : Stdlib.Format.formatter -> t -> unit
val empty : t
val is_empty : t -> Gillian.Gil_syntax.Expr.t
val sure_is_all_zeros : t -> bool
val equal : t -> t -> bool
val conc_to_abst_undelayed : SVal.t list -> Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t list
val concat : t -> t -> t option
val to_single_value : chunk:Chunk.t -> t -> t option Monadic.Delayed.t

This already assumes the value is a number and not a pointer

val singleton : t -> t
val array_cons : SVal.t -> t -> t option

This assumes chunks are properly respected outside of the call of this function

val array_append : t -> t -> t option
val of_gil_expr_exn : Gillian.Gil_syntax.Expr.t -> t
val learn_chunk : chunk:Chunk.t -> size:Gillian.Gil_syntax.Expr.t -> t -> unit Monadic__Delayed.t

Only call on Mint8Unsigned arrays

val subst : le_subst:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) -> t -> t