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.

1 files changed, 15 insertions, 6 deletions

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 =