diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-19 11:26:31 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-04-19 11:26:31 +0200 |
commit | e6744b2bf013158c5158580107530eee65b53b35 (patch) | |
tree | 3e4ff1c482a6aecd3c483bc31cd46a272b6d8144 /cparser | |
parent | 6106e043c8a13bf882d2227b3ee80a108305d8df (diff) | |
download | compcert-kvx-e6744b2bf013158c5158580107530eee65b53b35.tar.gz compcert-kvx-e6744b2bf013158c5158580107530eee65b53b35.zip |
Ensure compatibility with future versions of MenhirLib
After Menhir version 20210310, the `Fail_pr` constructor of the
`parse_result` type becomes `Fail_pr_full` with two extra arguments.
This PR enables CompCert to handle both versions of the `parse_result`
type in MenhirLib.
Diffstat (limited to 'cparser')
-rw-r--r-- | cparser/Parse.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/cparser/Parse.ml b/cparser/Parse.ml index d9f9aa1c..3ed193f9 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -72,12 +72,13 @@ let preprocessed_file transfs name sourcefile = (fun () -> Parser.translation_unit_file log_fuel (Lexer.tokens_stream name text)) () with - | Parser.MenhirLibParser.Inter.Fail_pr -> - (* Theoretically impossible : implies inconsistencies - between grammars. *) - Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing" - | Parser.MenhirLibParser.Inter.Timeout_pr -> assert false - | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast) in + | Parser.MenhirLibParser.Inter.Parsed_pr (ast, _ ) -> ast + | _ -> (* Fail_pr or Fail_pr_full or Timeout_pr, depending + on the version of Menhir. + Fail_pr{,_full} means that there's an inconsistency + between the pre-parser and the parser. + Timeout_pr means that we ran for 2^50 steps. *) + Diagnostics.fatal_error Diagnostics.no_loc "internal error while parsing") in let p1 = Timing.time "Elaboration" Elab.elab_file ast in Diagnostics.check_errors (); Timing.time2 "Emulations" transform_program t p1 name in |