gillian » Gillian » Gil_syntax » BiSpec

Module Gil_syntax.BiSpec

type t = {

1. bispec_name : string;
   (*

   Procedure/spec name

   *)
2. bispec_params : string list;
   (*

   Procedure/spec parameters

   *)
3. bispec_pres : Asrt.t Utils.Location.located 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 ->
  Asrt.t Utils.Location.located list ->
  bool ->
  t

val init_tbl : unit -> t_tbl

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer