Parameter Make.PC

module TargetLangOptions : sig ... end
type init_data = SPState.init_data
type err

Type of error that can occur during parsing or compilation

type tl_ast

Type of the target language AST

Type of the TL's GIL annotations

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) Gillian.Command_line.ParserAndCompiler.compiled_progs, err) Stdlib.result

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) Gillian.Gil_syntax.Prog.t, err) Stdlib.result)) 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 : Gillian.Utils.Exec_mode.t -> unit

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