gillian » Gillian » Debugger » Lifter » Gil_fallback_lifter » Make » V

Parameter Make.V

type heap_t

type state

type m_err

type annot = PC.Annot.t

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

module SState :
  Engine.SState.S with type t = SPState.state_t and type heap_t = heap_t

module SAInterpreter :
  General.G_interpreter.S
    with type vt = Symbolic.Values.t
     and type st = 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 with type state_t = SPState.state_t

type t

type prog_t = (annot, int) 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 Utils.Gillian_result.t

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