Module Gil_syntax.Prog

A full GIL program

type ('annot, 'label) t = {
  1. imports : (string * bool) list;
    (*

    List of imported GIL files, and whether each has to be verified

    *)
  2. lemmas : (string, Lemma.t) Utils.Prelude.Hashtbl.t;
    (*

    Lemmas

    *)
  3. preds : (string, Pred.t) Utils.Prelude.Hashtbl.t;
    (*

    Predicates

    *)
  4. only_specs : (string, Spec.t) Utils.Prelude.Hashtbl.t;
    (*

    Specs without function definitions

    *)
  5. procs : (string, ('annot, 'label) Proc.t) Utils.Prelude.Hashtbl.t;
    (*

    Proceudes

    *)
  6. macros : (string, Macro.t) Utils.Prelude.Hashtbl.t;
    (*

    Macros

    *)
  7. bi_specs : (string, BiSpec.t) Utils.Prelude.Hashtbl.t;
    (*

    Bi-abductive specs

    *)
  8. proc_names : string list;
    (*

    Names of the procedures

    *)
  9. predecessors : (string * int * int, int) Utils.Prelude.Hashtbl.t;
    (*

    Table used for Phi-assignment

    *)
}
val make : imports:(string * bool) list -> lemmas:(string, Lemma.t) Utils.Prelude.Hashtbl.t -> preds:(string, Pred.t) Utils.Prelude.Hashtbl.t -> only_specs:(string, Spec.t) Utils.Prelude.Hashtbl.t -> procs:(string, ('annot, 'label) Proc.t) Utils.Prelude.Hashtbl.t -> macros:(string, Macro.t) Utils.Prelude.Hashtbl.t -> bi_specs:(string, BiSpec.t) Utils.Prelude.Hashtbl.t -> proc_names:string list -> predecessors:(string * int * int, int) Utils.Prelude.Hashtbl.t -> unit -> ('annot, 'label) t

Makes a full program

val make_labeled : procs:(string, ('annot, string) Proc.t) Utils.Prelude.Hashtbl.t -> imports:(string * bool) list -> lemmas:(string, Lemma.t) Utils.Prelude.Hashtbl.t -> preds:(string, Pred.t) Utils.Prelude.Hashtbl.t -> only_specs:(string, Spec.t) Utils.Prelude.Hashtbl.t -> macros:(string, Macro.t) Utils.Prelude.Hashtbl.t -> bi_specs:(string, BiSpec.t) Utils.Prelude.Hashtbl.t -> proc_names:string list -> unit -> ('annot, string) t

Initialises a labeled program (with empty predecessors, to be computed later)

val make_indexed : procs:('annot, int) Proc.t list -> predecessors:(string * int * int * int) list -> lemmas:(string, Lemma.t) Utils.Prelude.Hashtbl.t -> preds:(string, Pred.t) Utils.Prelude.Hashtbl.t -> only_specs:(string, Spec.t) Utils.Prelude.Hashtbl.t -> macros:(string, Macro.t) Utils.Prelude.Hashtbl.t -> bi_specs:(string, BiSpec.t) Utils.Prelude.Hashtbl.t -> unit -> ('annot, int) t

Initialises an indexed program (with empty proc_names and imports, useless for the rest)

val create : unit -> ('a, string) t

Creates an empty program

val get_lemmas : ('a, 'b) t -> Lemma.t list

Getters

Get all lemmas

val get_preds : ('a, 'b) t -> Pred.t list

Get all predicates

val get_ospecs : ('a, 'b) t -> Spec.t list

Get all only-specs

val get_specs : ('a, 'b) t -> Spec.t list

Get all specs

val get_procs : ?proc_names:string list -> ('a, 'b) t -> ('a, 'b) Proc.t list

Get all procedures

val get_bispecs : ('a, 'b) t -> BiSpec.t list

Get all bi-abductive specs

val get_proc_names : ('a, 'b) t -> string list

Get names of all procedures

val get_noninternal_proc_names : ('a, 'b) t -> string list

Get names of all procedures not marked as internal

val get_noninternal_pred_names : ('a, 'b) t -> string list

Get names of all predicates not marked as internal

val get_noninternal_lemma_names : ('a, 'b) t -> string list

Get names of all lemmas not marked as internal

val get_proc : ('a, 'b) t -> string -> ('a, 'b) Proc.t option

Get a specific procedure

val get_proc_exn : ('a, 'b) t -> string -> ('a, 'b) Proc.t

Get a specific procedure. Raises Failure if it does not exist

val get_pred : ('a, 'b) t -> string -> Pred.t option

Get a specific predicate

val get_pred_exn : ('a, 'b) t -> string -> Pred.t

Get a specific predicate. Raises Failure if it does not exist

val get_bispec : ('a, 'b) t -> string -> BiSpec.t option

Get a specific bi-abductive spec

val get_bispec_exn : ('a, 'b) t -> string -> BiSpec.t

Get a specific bi-abductive spec. Raises Failure if it does not exist

val get_lemma : ('a, 'b) t -> string -> Lemma.t option

Get a specific lemma

val get_lemma_exn : ('a, 'b) t -> string -> Lemma.t

Get a specific lemma. Raises Failure if it does not exist

Setters

val update_specs : ('a, 'b) t -> ('c, 'd) t -> unit

Add specs

val update_imports : ('a, 'b) t -> (string * bool) list -> ('a, 'b) t

Add imports

val add_lemma : ('a, 'b) t -> Lemma.t -> ('a, 'b) t

Add a lemma

val add_pred : ('a, 'b) t -> Pred.t -> ('a, 'b) t

Add a predicate

val add_ospec : ('a, 'b) t -> Spec.t -> ('a, 'b) t

Add an only-spec

val add_proc : ('a, 'b) t -> ('a, 'b) Proc.t -> ('a, 'b) t

Add a proc

val add_macro : ('a, 'b) t -> Macro.t -> ('a, 'b) t

Add a macro

val add_bispec : ('a, 'b) t -> BiSpec.t -> ('a, 'b) t

Add a bi-abductive spec

val pp : show_labels:bool -> pp_label:'b Fmt.t -> ?pp_annot:'a Fmt.t -> Stdlib.Format.formatter -> ('a, 'b) t -> unit

Printers

val pp_labeled : Stdlib.Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, string) t -> unit

Print labelled

val pp_indexed : Stdlib.Format.formatter -> ?pp_annot:'a Fmt.t -> ('a, int) t -> unit

Print indexed