Module ActionAdder.Make

Parameters

module A : ActionAddition
module S : MyMonadicSMemory.S with type t = A.t

Signature

include module type of struct include S end
type t = A.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type pred = S.pred
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val empty : unit -> t

Returns an empty state

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.

The set of logical variables in the state

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_preds : unit -> (pred * string list * string list) list

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

type action =
  1. | BaseAct of S.action
  2. | AddedAct of A.action
type err_t =
  1. | BaseErr of S.err_t
  2. | AddedErr of A.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
val _ : Yojson.Safe.t -> err_t Ppx_deriving_yojson_runtime.error_or
val list_actions : unit -> (action * string list * string list) list
val action_from_str : string -> action option
val action_to_str : action -> string
val map_base_err : ('a, S.err_t) Stdlib.result Gillian.Monadic.Delayed.t -> ('a, err_t) Stdlib.result Gillian.Monadic.Delayed.t
val map_added_err : ('a, A.err_t) Stdlib.result Gillian.Monadic.Delayed.t -> ('a, err_t) Stdlib.result Gillian.Monadic.Delayed.t
val execute_action : action -> S.t -> Gillian.Gil_syntax.Expr.t list -> (S.t * Gillian.Gil_syntax.Expr.t list, err_t) Stdlib.result Gillian.Monadic.Delayed.t
val can_fix : err_t -> bool
val get_fixes : err_t -> S.pred MyAsrt.t list list