gillian » Gillian » Command_line » ParserAndCompiler » S

Module type ParserAndCompiler.S

module TargetLangOptions : sig ... end

type init_data

type err

Type of error that can occur during parsing or compilation

type tl_ast

Type of the target language AST

module Annot : Gil_syntax.Annot.S

val pp_err : Stdlib.Format.formatter -> err -> unit

Pretty printer for type err

val parse_and_compile_files :
  string list ->
  (Annot.t, tl_ast, init_data) ParserAndCompiler.compiled_progs
    Utils.Gillian_result.t

Takes a set of source file paths, parses them with the user's language, and then compiles them to a single or a set of GIL programs. The returned GIL program(s) should be ready to be analysed.

val other_imports :
  (string
   * (string ->
   (Annot.t, string) Gil_syntax.Prog.t Utils.Gillian_result.t))
    list

other_imports is an association list that maps extensions to a parser and compiler. For example, it is possible to import a JSIL file in a GIL program using import "file.jsil";. In order to do so, the other_imports list should contain the tuple ("jsil", parse_and_compile_jsil_file) where parse_and_compile_jsil_file is a function that takes a file path, parses the file as a JSIL program, and compiles this to a GIL program.

val default_import_paths : string list option

Contains the name of the environment variable which contains the path to where the runtime is stored.

val initialize : Utils.Exec_mode.t -> unit

Function that will be executed at initialisation. It will be passed the current execution mode as parameter