Module Cgil_lib.MonadicSVal

include module type of struct include SVal end
val let* : 'a option -> ('a -> 'b option) -> 'b option
val let+ : 'a option -> ('a -> 'b) -> 'b option
type t = SVal.t =
  1. | SUndefined
  2. | Sptr of string * Gillian.Gil_syntax.Expr.t
  3. | SVint of Gillian.Gil_syntax.Expr.t
  4. | SVlong of Gillian.Gil_syntax.Expr.t
  5. | SVsingle of Gillian.Gil_syntax.Expr.t
  6. | SVfloat of Gillian.Gil_syntax.Expr.t
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 equal : t -> t -> bool
type typ = Compcert.AST.typ =
  1. | Tint
  2. | Tfloat
  3. | Tlong
  4. | Tsingle
  5. | Tany32
  6. | Tany64
val tptr : Compcert.AST.typ
val is_loc : Gillian.Symbolic.Type_env.t -> string -> bool
val is_zero : t -> bool
val zero_of_chunk : Chunk.t -> t
val is_loc_ofs : Gillian.Symbolic.Type_env.t -> string -> string -> bool
val of_gil_expr_almost_concrete : ?gamma:Gillian.Symbolic.Type_env.t -> Gillian.Gil_syntax.Expr.t -> (t * Gillian.Gil_syntax.Expr.t list) option
val lvars : t -> Utils.Containers.SS.t
val alocs : t -> Utils.Containers.SS.t
val pp : Stdlib.Format.formatter -> t -> unit
val substitution : le_subst:(Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t) -> t -> t
exception NotACompCertValue of Gillian.Gil_syntax.Expr.t
module Patterns : sig ... end
val of_chunk_and_expr : Chunk.t -> Gillian.Gil_syntax.Expr.t -> t Monadic__Delayed.t
val of_gil_expr : Gillian.Gil_syntax.Expr.t -> t option Monadic__Delayed.t
val of_gil_expr_exn : Gillian.Gil_syntax.Expr.t -> t Monadic__Delayed.t
val of_gil_expr_vanish : Gillian.Gil_syntax.Expr.t -> t Monadic__Delayed.t
val sure_is_zero : t -> bool
module SVArray : sig ... end
module Infix : sig ... end