aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CMlexer.mll
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2016-03-15 14:58:05 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2016-03-15 14:58:05 +0100
commit2f31ded1ab2a78f1362b95b6079023c94909fe6b (patch)
tree9e82aa407d26fcea434ed23d28ae09d5dca41574 /backend/CMlexer.mll
parentd58c35ebb8c3124d67c51091bb6e4cfedc59d999 (diff)
downloadcompcert-2f31ded1ab2a78f1362b95b6079023c94909fe6b.tar.gz
compcert-2f31ded1ab2a78f1362b95b6079023c94909fe6b.zip
GPR#84: extend Cminor parser to handle single-precision FP operations
Diffstat (limited to 'backend/CMlexer.mll')
-rw-r--r--backend/CMlexer.mll5
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 6695b6b7..a595311a 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -123,6 +123,7 @@ rule token = parse
| "-" { MINUS }
| "->" { MINUSGREATER }
| "-f" { MINUSF }
+ | "-s" { MINUSS }
| "-l" { MINUSL }
| "%" { PERCENT }
| "%l" { PERCENTL }
@@ -130,6 +131,7 @@ rule token = parse
| "%u" { PERCENTU }
| "+" { PLUS }
| "+f" { PLUSF }
+ | "+s" { PLUSS }
| "+l" { PLUSL }
| "}" { RBRACE }
| "}}" { RBRACERBRACE }
@@ -140,13 +142,16 @@ rule token = parse
| ";" { SEMICOLON }
| "/" { SLASH }
| "/f" { SLASHF }
+ | "/s" { SLASHS }
| "/l" { SLASHL }
| "/lu" { SLASHLU }
| "/u" { SLASHU }
| "single" { SINGLE }
+ | "singleofint" { SINGLEOFINT }
| "stack" { STACK }
| "*" { STAR }
| "*f" { STARF }
+ | "*s" { STARS }
| "*l" { STARL }
| "switch" { SWITCH }
| "switchl" { SWITCHL }