Module Gil_syntax.BiSpec

Bi-abductive specifications

type t = {
  1. bispec_name : string;
    (*

    Procedure/spec name

    *)
  2. bispec_params : string list;
    (*

    Procedure/spec parameters

    *)
  3. bispec_pres : Gillian.Gil_syntax.Asrt.t list;
    (*

    Possible preconditions

    *)
  4. bispec_normalised : bool;
    (*

    If the spec is already normalised

    *)
}
type t_tbl = (string, t) Utils.Prelude.Hashtbl.t
val init : string -> string list -> Gillian.Gil_syntax.Asrt.t list -> bool -> t
val init_tbl : unit -> t_tbl
val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer