Module Cgil_lib.MonadicSMemory

include Gillian.Monadic.MonadicSMemory.S with type init_data = Global_env.t
type init_data = Global_env.t

Type of GIL values

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 copy : t -> t

State Copy

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

Printer

val substitution_in_place : st -> t -> t Monadic.Delayed.t
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
val mem_constraints : t -> Gillian.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 -> Gillian.Gil_syntax.Expr.t
val get_fixes : err_t -> Gillian.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 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

module Lift : sig ... end