Make.State
include Gillian.General.State.S
with type vt = Gillian.Gil_syntax.Expr.t
and type st = Gillian.Symbolic.Subst.t
and type store_t = SStore.t
type vt = Gillian.Gil_syntax.Expr.t
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
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type st = Gillian.Symbolic.Subst.t
Type of GIL substitutions
type store_t = SStore.t
Type of GIL stores
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) 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
type action_ret = (t * vt list, err_t) 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
val execute_action : string -> t -> vt list -> action_ret
val eval_expr : t -> Gillian.Gil_syntax.Expr.t -> vt
Expression Evaluation
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_f : t -> Gillian.Gil_syntax.Formula.t list -> st option
val assert_a : t -> Gillian.Gil_syntax.Formula.t list -> bool
Assert assertion
val get_type : t -> vt -> Gillian.Gil_syntax.Type.t option
State simplification
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 Recovery_tactic.t
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 evaluate_slcmd :
'a MP.prog ->
Gillian.Gil_syntax.SLCmd.t ->
t ->
(t, err_t) Res_list.t
val match_invariant :
'a MP.prog ->
bool ->
t ->
Gillian.Gil_syntax.Asrt.t ->
string list ->
(t * t, err_t) 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) Res_list.t
val run_spec :
MP.spec ->
t ->
string ->
vt list ->
(string * (string * vt) list) option ->
(t * Gillian.Gil_syntax.Flag.t, err_t) Res_list.t
val unfolding_vals : t -> Gillian.Gil_syntax.Formula.t list -> vt list
val try_recovering :
t ->
vt Recovery_tactic.t ->
(t list, string) Stdlib.result
val clean_up : ?keep:Gil_syntax.Expr.Set.t -> t -> unit
val produce_posts : t -> st -> Gillian.Gil_syntax.Asrt.t list -> t list
val produce : t -> st -> Gillian.Gil_syntax.Asrt.t -> (t, err_t) Res_list.t
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 make_s :
init_data:init_data ->
store:store_t ->
pfs:Symbolic.Pure_context.t ->
gamma:Symbolic.Type_env.t ->
spec_vars:Utils.Prelude.SS.t ->
t
val get_typ_env : t -> Symbolic.Type_env.t
val get_pfs : t -> Symbolic.Pure_context.t
val sure_is_nonempty : t -> bool
val consume_core_pred : string -> t -> vt list -> action_ret