gillian » Gillian » Command_line

Module Gillian.Command_line

module ParserAndCompiler : sig ... end

This defines an interface that allows a user to indicate how to parse their own programming language, preprocess the obtained language and compile it to GIL (type Prog.t)

module Make
  (ID : Engine.Init_data.S)
  (CMemory : Concrete.Memory_S with type init_data = ID.t)
  (SMemory : Engine.SMemory.S with type init_data = ID.t)
  (PC : Command_line.ParserAndCompiler.S with type init_data = ID.t)
  (External : Engine.External.T(PC.Annot).S)
  (Runners : sig ... end)
  (Lifter :
    functor (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) :
  sig ... end