gillian » Gillian » Command_line » Make

Module Command_line.Make

Parameters

moduleID : Engine.Init_data.S

moduleCMemory : Concrete.Memory_S with type init_data = ID.t

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

modulePC : Command_line.ParserAndCompiler.S with type init_data = ID.t

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

moduleRunners : sig ... end

moduleLifter
  (V : Engine.Verifier.S with type annot = PC.Annot.t) :
  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