Module Jsil_syntax.Spec

module SSubst = Gillian.Symbolic.Subst
type st = {
  1. pre : Asrt.t;
    (*

    Precondition

    *)
  2. posts : Asrt.t list;
    (*

    Postcondition

    *)
  3. flag : Flag.t;
    (*

    Return flag (jsil_return_flag)

    *)
  4. to_verify : bool;
    (*

    Should the spec be verified?

    *)
  5. label : (string * SS.t) option;
}

Single JSIL specifications.

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

    Procedure/spec name

    *)
  2. params : string list;
    (*

    Procedure/spec parameters

    *)
  3. sspecs : st list;
    (*

    List of single specifications

    *)
  4. normalised : bool;
    (*

    If the spec is already normalised

    *)
  5. incomplete : bool;
    (*

    If the spec is incomplete

    *)
  6. to_verify : bool;
    (*

    Should the spec be verified?

    *)
}

Full JSIL specifications.

val s_init : ?label:(string * SS.t) -> Asrt.t -> Asrt.t list -> Flag.t -> bool -> st

Creates a JSIL specification given its components

val init : string -> string list -> st list -> bool -> bool -> bool -> t
val extend : t -> st list -> t
val get_params : t -> string list
val pp_sspec : Stdlib.Format.formatter -> st -> unit
val pp : Stdlib.Format.formatter -> t -> unit