Module Jsil_syntax.EProg

module L = Gillian.Logging
type t = {
  1. imports : (string * bool) list;
  2. lemmas : (string, Lemma.t) Stdlib.Hashtbl.t;
  3. preds : (string, Pred.t) Stdlib.Hashtbl.t;
  4. only_specs : (string, Spec.t) Stdlib.Hashtbl.t;
  5. procs : (string, EProc.t) Stdlib.Hashtbl.t;
  6. macros : (string, Macro.t) Stdlib.Hashtbl.t;
  7. bi_specs : (string, BiSpec.t) Stdlib.Hashtbl.t;
  8. proc_names : string list;
}
val init : (string * bool) list -> (string, Lemma.t) Stdlib.Hashtbl.t -> (string, Pred.t) Stdlib.Hashtbl.t -> (string, Spec.t) Stdlib.Hashtbl.t -> (string, EProc.t) Stdlib.Hashtbl.t -> (string, Macro.t) Stdlib.Hashtbl.t -> (string, BiSpec.t) Stdlib.Hashtbl.t -> string list -> t
val full_init : unit -> t
val get_lemmas : t -> Lemma.t list
val get_preds : t -> Pred.t list
val get_ospecs : t -> Spec.t list
val get_specs : t -> Spec.t list
val get_procs : ?proc_names:string list -> t -> EProc.t list
val get_proc : t -> string -> EProc.t option
val get_bispecs : t -> BiSpec.t list
val pp : Stdlib.Format.formatter -> t -> unit
val update_imports : t -> string list -> t
val add_lemma : t -> Lemma.t -> t
val add_pred : t -> Pred.t -> t
val add_ospec : t -> Spec.t -> t
val add_proc : t -> EProc.t -> t
val add_macro : t -> Macro.t -> t
val add_bispec : t -> BiSpec.t -> t