gillian » Gillian » Gil_syntax » Spec

Module Gil_syntax.Spec

type st = {

1. ss_pre : Asrt.t Utils.Location.located;
   (*

   Precondition

   *)
2. ss_posts : Asrt.t Utils.Location.located list;
   (*

   Postcondition

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

   Variant

   *)
4. ss_flag : 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?

   *)
7. spec_location : Utils.Location.t option;

}

Full specification

val s_init :
  ?ss_label:(string * string list) ->
  Asrt.t Utils.Location.located ->
  Asrt.t Utils.Location.located list ->
  Expr.t option ->
  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 ->
  Utils.Location.t option ->
  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, 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