Legacy_symbolic (gillian-js.Semantics.Legacy

type init_data = unit

type vt = Gillian.Symbolic.Values.t

val vt_to_yojson : vt -> Yojson.Safe.t

val vt_of_yojson : Yojson.Safe.t -> vt Ppx_deriving_yojson_runtime.error_or

val pp_vt : 
  Ppx_deriving_runtime.Format.formatter ->
  vt ->
  Ppx_deriving_runtime.unit

val show_vt : vt -> Ppx_deriving_runtime.string

type t = SHeap.t

Type of JSIL general states

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val sure_is_nonempty : 'a -> bool

type st = Gillian.Symbolic.Subst.t

Type of JSIL substitutions

type i_fix_t =

| FLoc of vt
| FCell of vt * vt
| FMetadata of vt
| FPure of Gillian.Gil_syntax.Expr.t

Errors

val i_fix_t_to_yojson : i_fix_t -> Yojson.Safe.t

val i_fix_t_of_yojson : 
  Yojson.Safe.t ->
  i_fix_t Ppx_deriving_yojson_runtime.error_or

val pp_i_fix_t : 
  Ppx_deriving_runtime.Format.formatter ->
  i_fix_t ->
  Ppx_deriving_runtime.unit

val show_i_fix_t : i_fix_t -> Ppx_deriving_runtime.string

type err_t = vt list * i_fix_t list list * Gillian.Gil_syntax.Expr.t

val err_t_to_yojson : err_t -> Yojson.Safe.t

val err_t_of_yojson : 
  Yojson.Safe.t ->
  err_t Ppx_deriving_yojson_runtime.error_or

val _ : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or

val pp_err_t : 
  Ppx_deriving_runtime.Format.formatter ->
  err_t ->
  Ppx_deriving_runtime.unit

val show_err_t : err_t -> Ppx_deriving_runtime.string

type action_ret =
  ((t
    * vt list
    * Gillian.Gil_syntax.Expr.t list
    * (string * Gillian.Gil_syntax.Type.t) list)
     list,
    err_t list)
    Stdlib.result

val pp_i_fix : Stdlib.Format.formatter -> i_fix_t -> unit

val get_failing_constraint : err_t -> Gillian.Gil_syntax.Expr.t

val pp_err : Stdlib.Format.formatter -> err_t -> unit

val get_recovery_tactic : t -> err_t -> vt Gillian.General.Recovery_tactic.t

val assertions : ?to_keep:'a -> t -> Gillian.Gil_syntax.Asrt.t

val lvars : t -> Gillian.Utils.Containers.SS.t

val alocs : t -> Gillian.Utils.Containers.SS.t

val clean_up : 
  ?keep:Gillian.Gil_syntax.Expr.Set.t ->
  t ->
  Gillian.Gil_syntax.Expr.Set.t * Gillian.Gil_syntax.Expr.Set.t

val substitution_in_place : 
  pfs:'a ->
  gamma:'b ->
  st ->
  t ->
  (t * Gillian.Gil_syntax.Expr.Set.t * 'c list) list

val pp : Stdlib.Format.formatter -> t -> unit

val pp_by_need : 
  Utils.Prelude.SS.t ->
  Stdlib.Format.formatter ->
  SHeap.t ->
  unit

val get_print_info : 
  Utils.Prelude.SS.t ->
  SHeap.t ->
  Utils.Prelude.SS.t * Utils.Prelude.SS.t

val copy : t -> t

val init : unit -> t

val get_init_data : 'a -> unit

val clear : t -> t

val get_loc_name : 
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  Gillian.Gil_syntax.Expr.t ->
  string option

val fresh_loc : 
  ?loc:vt ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  string * vt * Gillian.Gil_syntax.Expr.t list

val alloc : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  vt option ->
  ?is_empty:bool ->
  vt option ->
  action_ret

val set_cell : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  vt ->
  vt ->
  action_ret

val get_cell : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  vt ->
  action_ret

val remove_cell : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  vt ->
  action_ret

val set_domain : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  vt ->
  action_ret

val get_metadata : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  action_ret

val set_metadata : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  vt ->
  action_ret

val delete_object : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  action_ret

val get_partial_domain : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  vt ->
  action_ret

val get_full_domain : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  action_ret

val remove_domain : 
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt ->
  action_ret

val execute_action : 
  ?matching:'a ->
  string ->
  t ->
  Gillian.Symbolic.Pure_context.t ->
  Gillian.Symbolic.Type_env.t ->
  vt list ->
  action_ret

val ga_to_setter : string -> string

val ga_to_getter : string -> string

val ga_to_deleter : string -> string

val mem_constraints : t -> Gillian.Gil_syntax.Expr.t list

val is_overlapping_asrt : string -> bool

val prop_abduce_none_in_js : string list

val prop_abduce_both_in_js : string list

val complete_fix_js : i_fix_t -> Gillian.Gil_syntax.Asrt.t list

val complete_fix_jsil : i_fix_t -> Gillian.Gil_syntax.Asrt.t list

val get_fixes : err_t -> Gillian.Gil_syntax.Asrt.t list

val can_fix : 'a -> bool

val sorted_locs_with_vals : 
  t ->
  (Gillian.Utils.Containers.SS.elt * SHeap.s_object) list