Module type MyMonadicSMemory.S

type t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
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 action
type pred
val action_from_str : string -> action option
val action_to_str : action -> string
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val empty : unit -> t

Returns an empty state

val execute_action : action -> t -> Gillian.Gil_syntax.Expr.t list -> (t * Gillian.Gil_syntax.Expr.t list, err_t) Stdlib.result Gillian.Monadic.Delayed.t

Execute an action

val consume : pred -> t -> Gillian.Gil_syntax.Expr.t list -> (t * Gillian.Gil_syntax.Expr.t list, err_t) Stdlib.result Gillian.Monadic.Delayed.t

Consume a predicate with the given ins

Produce a predicate with the given ins and outs

val compose : t -> t -> t Gillian.Monadic.Delayed.t

Compose two states together

val is_exclusively_owned : t -> Gillian.Gil_syntax.Expr.t list -> bool Gillian.Monadic.Delayed.t

For Freeable: if a state can be freed. Must only be true if no non-empty state can be composed with the state. The Expr list is irrelevant; it's required because of Gillian-C.

val is_empty : t -> bool

If this state is observably empty.

val is_concrete : t -> bool

If this state is entirely made up of concrete expressions.

val instantiate : Gillian.Gil_syntax.Expr.t list -> t * Gillian.Gil_syntax.Expr.t list

Instantiates this state with a list of arguments. This is used by PMap, either in static mode with the 'instantiate' action, or in dynamic mode when accessing a missing index.

val assertions : t -> (pred * Gillian.Gil_syntax.Expr.t list * Gillian.Gil_syntax.Expr.t list) list

The list of core predicates corresponding to the state.

val assertions_others : t -> Gillian.Gil_syntax.Asrt.atom list

The list of assertions that aren't core predicates corresponding to the state.

val can_fix : err_t -> bool

If the error can be fixed

val get_fixes : err_t -> pred MyAsrt.t list list

Get the fixes for an error, as a list of fixes -- a fix is a list of core predicates to produce onto the state.

The recovery tactic to attempt to resolve an error, by eg. unfolding predicates

val lvars : t -> Containers.SS.t

The set of logical variables in the state

val alocs : t -> Containers.SS.t

The set of abstract locations in the state

val substitution_in_place : Gillian.Symbolic.Subst.t -> t -> t Gillian.Monadic.Delayed.t

Applies a substitution to the state. This can branch, eg. when attempting to resolve equality of expressions.

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

Pretty print the state

val list_actions : unit -> (action * string list * string list) list

(Debug only) Return all available (action * arguments * outputs)

val list_preds : unit -> (pred * string list * string list) list

(Debug only) Return all available (predicates * ins * outs)