gillian » Gillian » General » State » S

Module type State.S

type vt

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

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 st

Type of GIL substitutions

type store_t

Type of GIL stores

type heap_t

type m_err_t

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

exceptionInternal_State_Error of err_t list * t

type action_ret = (t * vt list, err_t) Engine.Res_list.t

type init_data

val execute_action : string -> t -> vt list -> action_ret

val is_overlapping_asrt : string -> bool

val eval_expr : t -> 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 ->
  Gil_syntax.Expr.t list ->
  t option

Assume assertion

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

Assume type

val sat_check : t -> vt -> bool

Satisfiability check

val sat_check_f : t -> Gil_syntax.Expr.t list -> st option

val assert_a : t -> Gil_syntax.Expr.t list -> bool

Assert assertion

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

Value Equality

val get_type : t -> vt -> 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 -> Gil_syntax.Var.Set.t -> t

Add Spec Var

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

Get Spec Vars

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

Get all logical variables

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

Turns a state into a list of assertions

val evaluate_slcmd :
  'a Engine.MP.prog ->
  Gil_syntax.SLCmd.t ->
  t ->
  (t, err_t) Engine.Res_list.t

val match_invariant :
  'a Engine.MP.prog ->
  bool ->
  t ->
  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 ->
  string ->
  vt list ->
  (string * (string * vt) list) option ->
  t ->
  (t * Gil_syntax.Flag.t, err_t) Engine.Res_list.t

val run_par_spec :
  (Engine.MP.spec * string * vt list * (string * (string * vt) list) option)
    list ->
  t ->
  (t * Gil_syntax.Flag.t, err_t) Engine.Res_list.t

val sure_is_nonempty : t -> bool

val unfolding_vals : t -> Gil_syntax.Expr.t list -> vt list

val try_recovering :
  t ->
  vt Engine.Recovery_tactic.t ->
  (t list, string) Stdlib.result

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 -> Gil_syntax.Asrt.t list -> t list

val produce : t -> st -> Gil_syntax.Asrt.t -> (t, err_t) Engine.Res_list.t

val update_subst : t -> st -> unit

val mem_constraints : t -> Gil_syntax.Expr.t list

val can_fix : err_t -> bool

val get_failing_constraint : err_t -> Gil_syntax.Expr.t

val get_fixes : err_t -> Gil_syntax.Asrt.t list

val get_equal_values : t -> vt list -> vt list

val get_heap : t -> heap_t