From f1d236b83003eda71e12840732d159fd23b1b771 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 29 Apr 2014 13:58:18 +0000
Subject: Integration of Jacques-Henri Jourdan's verified parser. (Merge of
 branch newparser.)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cparser/Parse.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'cparser/Parse.ml')

diff --git a/cparser/Parse.ml b/cparser/Parse.ml
index 4a2ced2..61b5bc4 100644
--- a/cparser/Parse.ml
+++ b/cparser/Parse.ml
@@ -45,12 +45,20 @@ let preprocessed_file transfs name sourcefile =
     try
       let t = parse_transformations transfs in
       let lb = Lexer.init name ic in
-      let parse = Clflags.time2 "Parsing" Parser.file Lexer.initial lb in
-      let p1 = Clflags.time "Elaboration" Elab.elab_file parse in
+      let rec inf = Datatypes.S inf in
+      let ast : Cabs.definition list =
+        Obj.magic
+          (match Clflags.time2 "Parsing"
+                 Parser.translation_unit_file inf (Lexer.tokens_stream lb) with
+             | Parser.Parser.Inter.Fail_pr ->
+                 (* Theoretically impossible : implies inconsistencies
+                    between grammars. *)
+                 Cerrors.fatal_error "Internal error while parsing"
+             | Parser.Parser.Inter.Timeout_pr -> assert false
+             | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in
+      let p1 = Clflags.time "Elaboration" Elab.elab_file ast in
       Clflags.time2 "Emulations" transform_program t p1
     with
-    | Parsing.Parse_error ->
-        Cerrors.error "Error during parsing"; []
     | Cerrors.Abort ->
         [] in
   close_in ic;
-- 
cgit v1.2.3