diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2016-07-11 12:08:32 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-07-11 12:08:32 +0200 |
| commit | c9cbfda0506dfac791ff58ebb72fe56c333f8ad3 (patch) | |
| tree | 592be2bddc8f36e22cb7d4c2c1a2ae05ace50ae8 /backend | |
| parent | 4c7650c3eaf4dfbe5971864bf084e76f844051ee (diff) | |
| parent | 2ef43e7647ccd65a2a8f1d9fdd067a18e52c39cb (diff) | |
| download | compcert-c9cbfda0506dfac791ff58ebb72fe56c333f8ad3.tar.gz compcert-c9cbfda0506dfac791ff58ebb72fe56c333f8ad3.zip | |
Merge pull request #105 from m-schmidt/master
Fix parsing and handling of CMinor files
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CMlexer.mll | 1 | ||||
| -rw-r--r-- | backend/CMparser.mly | 4 |
2 files changed, 5 insertions, 0 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 } ; |