Make (gillian.Engine.Verifier.Make)

Parameters

module SState : 
  SState.S
    with type vt = Gillian.Symbolic.Values.t
     and type st = Gillian.Symbolic.Subst.t
     and type store_t = SStore.t

module SPState : PState.S with type state_t = SState.t and type init_data = SState.init_data

module PC : Gillian.Command_line.ParserAndCompiler.S

module External : Engine.External.T(PC.Annot).S

Signature

type heap_t = SPState.heap_t

type state = SPState.t

type m_err = SPState.m_err_t

type annot = PC.Annot.t

module SPState = SPState

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 = 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 : 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