Make (gillian.Command

Parameters

module ID : Engine.Init_data.S

module CMemory : Gillian.Concrete.Memory_S with type init_data = ID.t

module SMemory : Engine.SMemory.S with type init_data = ID.t

module PC : ParserAndCompiler.S with type init_data = ID.t

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

module Runners : sig ... end

module Lifter
  (V : Engine.Verifier.S with type annot = PC.Annot.t) : 
  Gillian.Debugger.Lifter.S
    with type memory = SMemory.t
     and type memory_error = SMemory.err_t
     and type tl_ast = PC.tl_ast
     and type cmd_report = V.SAInterpreter.Logging.ConfigReport.t
     and type annot = PC.Annot.t
     and type init_data = ID.t
     and type pc_err = PC.err

Signature

val main : unit -> unit

Parses command-line arguments and starts the requested Gillian execution