gillian » Gillian » Command_line » Make » SMemory

Parameter Make.SMemory

type init_data = ID.t

type vt := Symbolic.Values.t

Type of GIL values

type st := Symbolic.Subst.t

Type of GIL substitutions

type err_t

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

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

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, err_t) Stdlib.result

val init : init_data -> t

Initialisation

val get_init_data : t -> init_data

val clear : t -> t

val execute_action :
  action_name:string ->
  t ->
  vt list ->
  action_ret Monadic.Delayed.t

Execute action

val consume : core_pred:string -> t -> vt list -> action_ret Monadic.Delayed.t

val produce : core_pred:string -> t -> vt list -> t Monadic.Delayed.t

val is_overlapping_asrt : string -> bool

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

Printer

val substitution : st -> t -> t Monadic.Delayed.t

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

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

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

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

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

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

val get_failing_constraint : err_t -> Gil_syntax.Expr.t

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

val can_fix : err_t -> bool

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 sure_is_nonempty : t -> bool

val split_further :
  t ->
  string ->
  vt list ->
  err_t ->
  (vt list list * vt list) option

See SMemory.S.split_further