Verification (gillian.Debugger_utils.Match_map.Make

type heap_t

type state

type m_err

type annot

module SPState : 
  Engine.PState.S
    with type t = state
     and type heap_t = heap_t
     and type m_err_t = m_err

module SAInterpreter : 
  Gillian.General.G_interpreter.S
    with type vt = Gillian.Symbolic.Values.t
     and type st = Gillian.Symbolic.Subst.t
     and type store_t = Engine.SStore.t
     and type state_t = state
     and type heap_t = heap_t
     and type state_err_t = SPState.err_t
     and type annot = annot

module SMatcher : Engine.Matcher.S

type t

type prog_t = (annot, int) Gillian.Gil_syntax.Prog.t

type proc_tests = (string * t) list

val proc_tests_to_yojson : proc_tests -> Yojson.Safe.t

val start_time : float Stdlib.ref

val reset : unit -> unit

val verify_prog : 
  init_data:SPState.init_data ->
  prog_t ->
  bool ->
  IncrementalAnalysis.SourceFiles.t option ->
  unit

val verify_up_to_procs : 
  ?proc_name:string ->
  init_data:SPState.init_data ->
  prog_t ->
  SAInterpreter.result_t SAInterpreter.cont_func

val postprocess_files : IncrementalAnalysis.SourceFiles.t option -> unit

module Debug : sig ... end