diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 12:22:20 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-07-11 12:22:20 +0200 |
commit | 38829eb86eac1c9c3071decbaf9108e6c5737df9 (patch) | |
tree | fae620cd713ee520dfb201f4d76531bb518f141a | |
parent | 3872ce9f9806d9af334b1fde092145edf664d170 (diff) | |
parent | c9cbfda0506dfac791ff58ebb72fe56c333f8ad3 (diff) | |
download | compcert-38829eb86eac1c9c3071decbaf9108e6c5737df9.tar.gz compcert-38829eb86eac1c9c3071decbaf9108e6c5737df9.zip |
Merge branch 'master' of github.com:AbsInt/CompCert
-rw-r--r-- | backend/CMlexer.mll | 1 | ||||
-rw-r--r-- | backend/CMparser.mly | 4 | ||||
-rw-r--r-- | driver/Driver.ml | 48 |
3 files changed, 32 insertions, 21 deletions
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index c82f5401..65f244b5 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -136,6 +136,7 @@ rule token = parse | "]" { RBRACKET } | "readonly" { READONLY } | "return" { RETURN } + | "runtime" { RUNTIME } | ")" { RPAREN } | ";" { SEMICOLON } | "/" { SLASH } diff --git a/backend/CMparser.mly b/backend/CMparser.mly index 7fa6500a..94b50810 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -38,6 +38,8 @@ let mkef sg toks = EF_external(coqstring_of_camlstring s, sg) | [EFT_tok "builtin"; EFT_string s] -> EF_builtin(coqstring_of_camlstring s, sg) + | [EFT_tok "runtime"; EFT_string s] -> + EF_runtime(coqstring_of_camlstring s, sg) | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] -> EF_vload c | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] -> @@ -348,6 +350,7 @@ let mkmatch expr cases = %token READONLY %token RETURN %token RPAREN +%token RUNTIME %token SEMICOLON %token SINGLE %token SINGLEOFINT @@ -719,6 +722,7 @@ eftok: | VOLATILE { EFT_tok "volatile" } | EXTERN { EFT_tok "extern" } | BUILTIN { EFT_tok "builtin" } + | RUNTIME { EFT_tok "runtime" } | memory_chunk { EFT_chunk $1 } ; diff --git a/driver/Driver.ml b/driver/Driver.ml index 7311215d..a0ec07f1 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -86,29 +86,35 @@ let compile_cminor_file ifile ofile = Sections.initialize(); let ic = open_in ifile in let lb = Lexing.from_channel ic in - try - match Compiler.transf_cminor_program - (CMtypecheck.type_program - (CMparser.prog CMlexer.token lb)) with + (* Parse cminor *) + let cm = + try CMtypecheck.type_program (CMparser.prog CMlexer.token lb) + with Parsing.Parse_error -> + eprintf "File %s, character %d: Syntax error\n" + ifile (Lexing.lexeme_start lb); + exit 2 + | CMlexer.Error msg -> + eprintf "File %s, character %d: %s\n" + ifile (Lexing.lexeme_start lb) msg; + exit 2 + | CMtypecheck.Error msg -> + eprintf "File %s, type-checking error:\n%s" + ifile msg; + exit 2 in + (* Convert to Asm *) + let asm = + match Compiler.apply_partial + (Compiler.transf_cminor_program cm) + Asmexpand.expand_program with + | Errors.OK asm -> + asm | Errors.Error msg -> eprintf "%s: %a" ifile print_error msg; - exit 2 - | Errors.OK p -> - let oc = open_out ofile in - PrintAsm.print_program oc p; - close_out oc - with Parsing.Parse_error -> - eprintf "File %s, character %d: Syntax error\n" - ifile (Lexing.lexeme_start lb); - exit 2 - | CMlexer.Error msg -> - eprintf "File %s, character %d: %s\n" - ifile (Lexing.lexeme_start lb) msg; - exit 2 - | CMtypecheck.Error msg -> - eprintf "File %s, type-checking error:\n%s" - ifile msg; - exit 2 + exit 2 in + (* Print Asm in text form *) + let oc = open_out ofile in + PrintAsm.print_program oc asm; + close_out oc (* Processing of a .c file *) |