Old_memory (gillian.Engine.Legacy_s_memory.Modernize.Old

type init_data

Type of data that is given the first time memory is created. Useful when there's global context to know about like a type-system

type vt = Gillian.Symbolic.Values.t

Type of GIL values

type st = Gillian.Symbolic.Subst.t

Type of GIL substitutions

type err_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 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 t

Type of GIL general states

val to_yojson : t -> Yojson.Safe.t

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

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

val init : init_data -> t

Initialisation

val get_init_data : t -> init_data

val clear : t -> t

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

Execute action

val ga_to_setter : string -> string

val ga_to_getter : string -> string

val ga_to_deleter : string -> string

val is_overlapping_asrt : string -> bool

val copy : t -> t

State Copy

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

Printer

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

val get_print_info : 
  Utils.Containers.SS.t ->
  t ->
  Utils.Containers.SS.t * Utils.Containers.SS.t

val substitution_in_place : 
  pfs:Symbolic.Pure_context.t ->
  gamma:Symbolic.Type_env.t ->
  st ->
  t ->
  (t * Gil_syntax.Formula.Set.t * (string * Gillian.Gil_syntax.Type.t) list)
    list

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

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

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

val assertions : 
  ?to_keep:Utils.Containers.SS.t ->
  t ->
  Gillian.Gil_syntax.Asrt.t list

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

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

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

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

val can_fix : err_t -> bool

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

val sure_is_nonempty : t -> bool