Module Verification.SPState

include Engine.SState.S with type t = state with type heap_t = heap_t with type m_err_t = m_err
include Gillian.General.State.S with type vt = Gillian.Gil_syntax.Expr.t and type st = Gillian.Symbolic.Subst.t and type store_t = Engine.SStore.t with type t = state with type heap_t = heap_t with type m_err_t = m_err

Type of GIL values

val vt_to_yojson : vt -> Yojson.Safe.t
val vt_of_yojson : Yojson.Safe.t -> vt Ppx_deriving_yojson_runtime.error_or
val pp_vt : Ppx_deriving_runtime.Format.formatter -> vt -> Ppx_deriving_runtime.unit
val show_vt : vt -> Ppx_deriving_runtime.string
type t = state

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 of GIL substitutions

type store_t = Engine.SStore.t

Type of GIL stores

type heap_t = heap_t
type m_err_t = m_err

Errors

val m_err_t_to_yojson : m_err_t -> Yojson.Safe.t
val m_err_t_of_yojson : Yojson.Safe.t -> m_err_t Ppx_deriving_yojson_runtime.error_or
type err_t = (m_err_t, vt) Engine.StateErr.t
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 pp_err_t : Ppx_deriving_runtime.Format.formatter -> err_t -> Ppx_deriving_runtime.unit
val show_err_t : err_t -> Ppx_deriving_runtime.string
exception Internal_State_Error of err_t list * t
type action_ret = (t * vt list, err_t) Engine.Res_list.t
type variants_t = (string, Gillian.Gil_syntax.Expr.t option) Utils.Prelude.Hashtbl.t
val variants_t_to_yojson : variants_t -> Yojson.Safe.t
val variants_t_of_yojson : Yojson.Safe.t -> variants_t Ppx_deriving_yojson_runtime.error_or
type init_data
val execute_action : string -> t -> vt list -> action_ret
val is_overlapping_asrt : string -> bool
val eval_expr : t -> Gillian.Gil_syntax.Expr.t -> vt

Expression Evaluation

val get_store : t -> store_t

Get store of given symbolic state

val set_store : t -> store_t -> t

Set store of given symbolic state

val assume : ?unfold:bool -> t -> vt -> t list

Assume expression

val assume_a : ?matching:bool -> ?production:bool -> ?time:string -> t -> Gillian.Gil_syntax.Formula.t list -> t option

Assume assertion

val assume_t : t -> vt -> Gillian.Gil_syntax.Type.t -> t option

Assume type

val sat_check : t -> vt -> bool

Satisfiability check

val sat_check_f : t -> Gillian.Gil_syntax.Formula.t list -> st option
val assert_a : t -> Gillian.Gil_syntax.Formula.t list -> bool

Assert assertion

val equals : t -> vt -> vt -> bool

Value Equality

val get_type : t -> vt -> Gillian.Gil_syntax.Type.t option
val simplify : ?save:bool -> ?kill_new_lvars:bool -> ?matching:bool -> t -> st * t list

State simplification

val simplify_val : t -> vt -> vt

Value simplification

val fresh_loc : ?loc:vt -> t -> vt
val pp : Stdlib.Format.formatter -> t -> unit

Printers

val pp_by_need : Utils.Containers.SS.t -> Utils.Containers.SS.t -> Utils.Containers.SS.t -> Stdlib.Format.formatter -> t -> unit
val pp_err : Stdlib.Format.formatter -> err_t -> unit
val get_recovery_tactic : t -> err_t list -> vt Engine.Recovery_tactic.t
val copy : t -> t

State Copy

val add_spec_vars : t -> Gillian.Gil_syntax.Var.Set.t -> t

Add Spec Var

val get_spec_vars : t -> Gillian.Gil_syntax.Var.Set.t

Get Spec Vars

val get_lvars : t -> Gillian.Gil_syntax.Var.Set.t

Get all logical variables

val to_assertions : ?to_keep:Utils.Containers.SS.t -> t -> Gillian.Gil_syntax.Asrt.t list

Turns a state into a list of assertions

val match_invariant : 'a Engine.MP.prog -> bool -> t -> Gillian.Gil_syntax.Asrt.t -> string list -> (t * t, err_t) Engine.Res_list.t

match_invariant prog revisited state invariant binders returns a list of pairs of states. In each pair, the first element is the framed off state, and the second one is the invariant, i.e. the state obtained by producing the invariant

val frame_on : t -> (string * t) list -> string list -> (t, err_t) Engine.Res_list.t
val run_spec : Engine.MP.spec -> t -> string -> vt list -> (string * (string * vt) list) option -> (t * Gillian.Gil_syntax.Flag.t, err_t) Engine.Res_list.t
val unfolding_vals : t -> Gillian.Gil_syntax.Formula.t list -> vt list
val substitution_in_place : ?subst_all:bool -> st -> t -> t list
val clean_up : ?keep:Gil_syntax.Expr.Set.t -> t -> unit
val match_assertion : t -> st -> Engine.MP.step -> (t, err_t) Engine.Res_list.t
val produce_posts : t -> st -> Gillian.Gil_syntax.Asrt.t list -> t list
val update_subst : t -> st -> unit
val mem_constraints : t -> Gillian.Gil_syntax.Formula.t list
val can_fix : err_t -> bool
val get_failing_constraint : err_t -> Gillian.Gil_syntax.Formula.t
val get_fixes : err_t -> Gillian.Gil_syntax.Asrt.t list list
val get_equal_values : t -> vt list -> vt list
val get_heap : t -> heap_t
val make_s : init_data:init_data -> store:store_t -> pfs:Gillian.Symbolic.Pure_context.t -> gamma:Gillian.Symbolic.Type_env.t -> spec_vars:Utils.Prelude.SS.t -> t
val init : init_data -> t
val get_init_data : t -> init_data
val clear_resource : t -> t
val get_typ_env : t -> Gillian.Symbolic.Type_env.t
val sure_is_nonempty : t -> bool
val consume_core_pred : string -> t -> vt list -> action_ret
val produce_core_pred : string -> t -> vt list -> t list
val split_core_pred_further : t -> string -> vt list -> err_t -> (vt list list * vt list) option

See SMemory.S.split_further

type state_t
type abs_t = string * vt list
val make_p : preds:Engine.MP.preds_tbl_t -> init_data:init_data -> store:store_t -> pfs:Gillian.Symbolic.Pure_context.t -> gamma:Gillian.Symbolic.Type_env.t -> spec_vars:Utils.Prelude.SS.t -> unit -> t
val init_with_pred_table : Engine.MP.preds_tbl_t -> init_data -> t
val get_preds : t -> Engine.Preds.t

Get preds of given symbolic state

val set_preds : t -> Engine.Preds.t -> t

Set preds of given symbolic state

val set_wands : t -> Engine.Wands.t -> t

Set wands of given symbolic state

val set_variants : t -> variants_t -> t

Set variants of given symbolic state

val matches : t -> st -> Engine.MP.t -> Engine.Matcher.match_kind -> bool
val add_pred_defs : Engine.MP.preds_tbl_t -> t -> t
val get_all_preds : ?keep:bool -> (abs_t -> bool) -> t -> abs_t list
val set_pred : t -> abs_t -> unit
val try_recovering : t -> vt Engine.Recovery_tactic.t -> (t list, string) Stdlib.result