Module Jsil_syntax.BiSpec

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

    Procedure/spec name

    *)
  2. params : string list;
    (*

    Procedure/spec parameters

    *)
  3. pre : Asrt.t;
    (*

    Precondition

    *)
  4. normalised : bool;
    (*

    If the spec is already normalised

    *)
}

Single JSIL specifications.

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