diff options
| author | Michael Schmidt <github@mschmidt.me> | 2016-07-01 11:05:39 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2016-07-01 11:05:39 +0200 |
| commit | 948f5c7899acd1ecd1a948bd54b695c6fa3afafb (patch) | |
| tree | 122c105840b096621def3ebbe6d486f88e9b8f5f | |
| parent | a90b94b43e5d1ff99effc6af306987b5f559871b (diff) | |
| download | compcert-948f5c7899acd1ecd1a948bd54b695c6fa3afafb.tar.gz compcert-948f5c7899acd1ecd1a948bd54b695c6fa3afafb.zip | |
extend cminor parser to accept "extern runtime" declarations
| -rw-r--r-- | backend/CMparser.mly | 4 |
1 files changed, 4 insertions, 0 deletions
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 } ; |