From f8be3f5f2937b053b9cb75ada7937a6c1b20f019 Mon Sep 17 00:00:00 2001 From: François Pottier Date: Fri, 23 Oct 2015 13:34:43 +0200 Subject: Install the new system for reporting syntax errors. This requires the development version of Menhir, to be released soon. In summary: handcrafted.messages is new. It contains a mapping of erroneous sentences to error messages, together with a lot of comments. Makefile.extr is new. It contains a rule to generate cparser/pre_parser_messages.ml based on this mapping. cparser/ErrorReports.{ml,mli} are new. They construct syntax error messages, based on the compiled mapping. cparser/Lexer.mll is modified. The last two tokens that have been read are stored in a buffer. ErrorReports is called to construct a syntax error message. cparser/GNUmakefile is new. It offers several commands for working on the pre-parser. cparser/deLexer.ml is new. It is a script (it is not linked into CompCert). It translates the symbolic name of a token to an example of this token in concrete C syntax. It is used by [make -C cparser concrete] to produce the .c files in tests/generated/. cparser/tests/generated/Makefile is new. It runs ccomp, clang and gcc on each of the generated C files, so as to allow a comparison of the error messages. --- cparser/Lexer.mll | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) (limited to 'cparser/Lexer.mll') diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll index 62764a48..23d8ab8d 100644 --- a/cparser/Lexer.mll +++ b/cparser/Lexer.mll @@ -449,19 +449,24 @@ and singleline_comment = parse else initial lexbuf - (* [lexer tokens buffer] is a new lexer, which wraps [lexer], and also - records the token stream into the FIFO queue [tokens]. *) + (* [lexer tokens buffer] is a new lexer, which wraps [lexer], and also: 1- + records the token stream into the FIFO queue [tokens] and 2- records the + start and end positions of the last two tokens in the two-place buffer + [buffer]. *) - let lexer tokens : lexbuf -> Pre_parser.token = + let lexer tokens buffer : lexbuf -> Pre_parser.token = fun lexbuf -> let token = lexer lexbuf in Queue.push token tokens; + let startp = lexbuf.lex_start_p + and endp = lexbuf.lex_curr_p in + buffer := ErrorReports.update !buffer (startp, endp); token (* [invoke_pre_parser] is in charge of calling the pre_parser. It uses the incremental API, which allows us to do our own error handling. *) - let invoke_pre_parser filename text lexer = + let invoke_pre_parser filename text lexer buffer = let lexbuf = Lexing.from_string text in lexbuf.lex_curr_p <- {lexbuf.lex_curr_p with pos_fname = filename; pos_lnum = 1}; let module I = Pre_parser.MenhirInterpreter in @@ -469,14 +474,18 @@ and singleline_comment = parse and supplier = I.lexer_lexbuf_to_supplier lexer lexbuf and succeed () = () and fail checkpoint = - Cerrors.fatal_error_raw "syntax error" + Cerrors.fatal_error_raw "%s" (ErrorReports.report text !buffer checkpoint) in I.loop_handle succeed fail supplier checkpoint + (* [tokens_stream filename text] runs the pre_parser and produces a stream + of (appropriately classified) tokens. *) + let tokens_stream filename text : token coq_Stream = contexts_stk := [init_ctx]; let tokens = Queue.create () in - invoke_pre_parser filename text (lexer tokens); + let buffer = ref ErrorReports.Zero in + invoke_pre_parser filename text (lexer tokens buffer) buffer; assert (List.length !contexts_stk = 1); let rec compute_token_stream () = let loop t v = -- cgit