Module Gil_syntax.Spec

GIL specifications

type st = {
  1. ss_pre : Gillian.Gil_syntax.Asrt.t;
    (*

    Precondition

    *)
  2. ss_posts : Gillian.Gil_syntax.Asrt.t list;
    (*

    Postcondition

    *)
  3. ss_variant : Gillian.Gil_syntax.Expr.t option;
    (*

    Variant

    *)
  4. ss_flag : Gillian.Gil_syntax.Flag.t;
    (*

    Return flag

    *)
  5. ss_to_verify : bool;
    (*

    Should the spec be verified?

    *)
  6. ss_label : (string * string list) option;
}

Single specification

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

    Procedure/spec name

    *)
  2. spec_params : string list;
    (*

    Procedure/spec parameters

    *)
  3. spec_sspecs : st list;
    (*

    List of single specifications

    *)
  4. spec_normalised : bool;
    (*

    If the spec is already normalised

    *)
  5. spec_incomplete : bool;
    (*

    If the spec is incomplete

    *)
  6. spec_to_verify : bool;
    (*

    Should the spec be verified?

    *)
}

Full specification

val s_init : ?ss_label:(string * string list) -> Gillian.Gil_syntax.Asrt.t -> Gillian.Gil_syntax.Asrt.t list -> Gillian.Gil_syntax.Expr.t option -> Gillian.Gil_syntax.Flag.t -> bool -> st

s_init ~ss_label ss_pre ss_posts ss_flag ss_to_verify creates a single specification with the given values

val init : string -> string list -> st list -> bool -> bool -> bool -> t

init spec_name spec_params spec_sspecs spec_normalised spec_to_verify creates a full specification with the given values

val extend : t -> st list -> t

Extends a full specfiication with a single specification

val get_params : t -> string list

Return the list of parameters of a Spec

val pp_sspec : Stdlib.Format.formatter -> st -> unit
val pp : Stdlib.Format.formatter -> t -> unit
val parameter_types : (string, Gillian.Gil_syntax.Pred.t) Utils.Prelude.Hashtbl.t -> t -> t

Makes the types of parameters explicit in the assertions

val label_vars_to_set : ('a * Utils.Containers.SS.elt list) option -> ('a * Utils.Containers.SS.t) option
  • deprecated

    For legacy purposes, some functions use string sets instead of string list existentials. This function allows for a smooth translation

Serialization

val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> (t, string) Result.t
val hash_of_t : t -> string