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

Parameter Make.V

type heap_t

type m_err

type annot = PC.Annot.t

module State :
  Engine.SState.S with type heap_t = heap_t and type m_err_t = m_err

type state = State.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 = State.err_t
     and type annot = annot

module SMatcher : Engine.Matcher.S with type state_t = 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:State.init_data ->
  prog_t ->
  bool ->
  IncrementalAnalysis.SourceFiles.t option ->
  unit Utils.Gillian_result.t

val init_proc :
  init_data:State.init_data ->
  prog_t ->
  string ->
  SAInterpreter.result_t SAInterpreter.cont_func list

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

module Debug : sig ... end