gillian » Gillian » Utils » Call_graph

Module Utils.Call_graph

Type definitions

type t = Utils.Call_graph.t

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

type id = Utils.Call_graph.id

module IdSet = Utils.Call_graph.IdSet

General manipulations

val make : ?init_capacity:int -> unit -> t

val reset : t -> unit

val to_reverse_graph : t -> t

val merge : t -> t -> t

Getters and Setters

val add_proc : t -> string -> unit

val add_pred : t -> string -> unit

val add_lemma : t -> string -> unit

val add_proc_call : t -> string -> string -> unit

val add_pred_call : t -> string -> string -> unit

val add_lemma_call : t -> string -> string -> unit

val add_proc_pred_use : t -> string -> string -> unit

val add_proc_lemma_use : t -> string -> string -> unit

val add_lemma_pred_use : t -> string -> string -> unit

val get_children : t -> id -> id list

val get_proc_names : t -> string list

val get_pred_names : t -> string list

val get_lemma_names : t -> string list

val prune_procs : t -> string list -> unit

val prune_lemmas : t -> string list -> unit

Filters

val contains_proc : t -> string -> bool

val contains_pred : t -> string -> bool

val contains_lemma : t -> string -> bool

val is_pred : t -> id -> bool

val is_proc : t -> id -> bool

val is_lemma : t -> id -> bool

Name/id manipulation

val id_of_proc_name : string -> id

val id_of_pred_name : string -> id

val id_of_lemma_name : string -> id

val get_name : t -> id -> string

Sorting

val get_sorted_names : t -> string list

Serialization

val pp : Stdlib.Format.formatter -> t -> unit