SVal (gillian-c.Cgil

val let* : 'a option -> ('a -> 'b option) -> 'b option

val let+ : 'a option -> ('a -> 'b) -> 'b option

type t =

| SUndefined
| Sptr of string * Gillian.Gil_syntax.Expr.t
| SVint of Gillian.Gil_syntax.Expr.t
| SVlong of Gillian.Gil_syntax.Expr.t
| SVsingle of Gillian.Gil_syntax.Expr.t
| 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 =

| Tint
| Tfloat
| Tlong
| Tsingle
| Tany32
| 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 of_gil_expr : 
  ?pfs:Gillian.Symbolic.Pure_context.t ->
  ?gamma:Gillian.Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t ->
  (t * Gillian.Gil_syntax.Expr.t list) option

val of_gil_expr_exn : 
  ?pfs:Gillian.Symbolic.Pure_context.t ->
  ?gamma:Gillian.Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t ->
  t * Gillian.Gil_syntax.Expr.t list

val to_gil_expr : 
  t ->
  Gillian.Gil_syntax.Expr.t
  * (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Type.t) list

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