Module IncrementalAnalysis.ChangeTracker

type proc_changes = {
  1. changed_procs : string list;
  2. new_procs : string list;
  3. deleted_procs : string list;
  4. dependent_procs : string list;
}
type lemma_changes = {
  1. changed_lemmas : string list;
  2. new_lemmas : string list;
  3. deleted_lemmas : string list;
  4. dependent_lemmas : string list;
}
val pp_proc_changes : Stdlib.Format.formatter -> proc_changes -> unit
val get_changes : ('a, 'b) Gillian.Gil_syntax.Prog.t -> prev_source_files:SourceFiles.t -> prev_call_graph:Gillian.Utils.Call_graph.t -> cur_source_files:SourceFiles.t -> proc_changes
val get_sym_changes : ('a, 'b) Gillian.Gil_syntax.Prog.t -> prev_source_files:SourceFiles.t -> prev_call_graph:Gillian.Utils.Call_graph.t -> cur_source_files:SourceFiles.t -> proc_changes
val get_verif_changes : ('a, 'b) Gillian.Gil_syntax.Prog.t -> prev_source_files:SourceFiles.t -> prev_call_graph:Gillian.Utils.Call_graph.t -> cur_source_files:SourceFiles.t -> proc_changes * lemma_changes
val get_callers : ('a, 'b) Gillian.Gil_syntax.Prog.t -> reverse_graph:Gillian.Utils.Call_graph.t -> excluded_procs:string list -> proc_name:string -> string list

Finds the closest, non-internal callers of proc_name using the given reverse call graph, ignoring any procedures in excluded_procs along the way.