Module Semantics.SHeap

JSIL Symbolic Heap

module SSubst = Gillian.Symbolic.Subst
module L = Logging
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 is_c : Gillian.Gil_syntax.Expr.t -> bool
val merge : 't option -> 't option -> ('t -> 't -> 't) -> 't option
val get_dom : t -> string -> Gillian.Gil_syntax.Expr.t option
val get_met : t -> string -> Gillian.Gil_syntax.Expr.t option
val set_fvl : t -> string -> Gillian.Gil_syntax.Expr.t Gillian.Gil_syntax.Expr.Map.t -> unit
val set_dom : t -> string -> Gillian.Gil_syntax.Expr.t option -> unit
val set_met : t -> string -> Gillian.Gil_syntax.Expr.t option -> unit

Symbolic heap functions *

val init : unit -> t

Returns an empty symbolic heap

val get : t -> string -> s_object option

Symbolic heap read heap(loc)

val get_with_default : t -> string -> s_object

Symbolic heap read heap(loc) with the normal new obj default

Symbolic heap set heap(loc) is assigned to fv_list

val set_fv_pair : t -> string -> Gillian.Gil_syntax.Expr.t -> Gillian.Gil_syntax.Expr.t -> unit

Symbolic heap put heap (loc, (perm, field)) is assigned to value

val init_object : t -> string -> ?is_empty:bool -> Gillian.Gil_syntax.Expr.t option -> unit
val has_loc : t -> string -> bool
val remove : t -> string -> unit

Removes the fv-list associated with --loc-- in --heap--

val domain : t -> Utils.Prelude.SS.t

Retrieves the domain of --heap--

val cdomain : t -> Utils.Prelude.SS.t
val copy : t -> t

Returns a copy of --heap--

val merge_loc : t -> string -> string -> unit
val substitution_in_place : SSubst.t -> t -> unit

Modifies --heap-- in place updating it to subst(heap)

val to_list : t -> (string * s_object) list

Returns the serialization of --heap-- as a list

val assertions : t -> Gillian.Gil_syntax.Asrt.t

converts a symbolic heap to a list of assertions

val wf_assertions_of_obj : t -> string -> Gillian.Gil_syntax.Expr.t list
val wf_assertions : t -> Gillian.Gil_syntax.Expr.t list
val is_well_formed : t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
val pp_by_need : Utils.Prelude.SS.t -> Stdlib.Format.formatter -> t -> unit
val clean_up : t -> unit