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

1 files changed, 12 insertions, 4 deletions

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;