Module States.Fractional

module Recovery_tactic = Gillian.General.Recovery_tactic

Value * Fraction

val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type err_t =
  1. | MissingState
  2. | NotEnoughPermission
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
type action =
  1. | Load
  2. | Store
type pred =
  1. | Frac
val action_from_str : string -> action option
val action_to_str : action -> string
val list_actions : unit -> (action * string list * string list) list
val pred_from_str : string -> pred option
val pred_to_str : pred -> string
val list_preds : unit -> (pred * string list * string list) list
val empty : unit -> t
val consume : pred -> ('a * Gillian.Gil_syntax.Expr.t) option -> Gillian.Gil_syntax.Expr.t list -> (('a * Gillian.Gil_syntax.Expr.t) option * 'a list, err_t) Stdlib.result Gillian.Monadic.Delayed.t
val compose : t -> t -> t Gillian.Monadic.Delayed.t
val is_exclusively_owned : ('a * Gillian.Gil_syntax.Expr.t) option -> 'b -> bool Gillian.Monadic.Delayed.t
val is_empty : 'a option -> bool
val is_concrete : (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option -> bool
val instantiate : 'a list -> (Gillian.Gil_syntax.Expr.t * Gillian.Gil_syntax.Expr.t) option * 'b list
val assertions : ('a * 'b) option -> (pred * 'b list * 'a list) list
val assertions_others : 'a -> 'b list
val get_recovery_tactic : 'a -> 'b Recovery_tactic.t
val can_fix : 'a -> bool
val get_fixes : 'a -> 'b list