diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-17 07:52:12 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-08-17 07:52:12 +0000 |
commit | 17f519651feb4a09aa90c89c949469e8a5ab0e88 (patch) | |
tree | c7bda5e43a2d1f950180521a1b854ac9592eea73 /backend/CMlexer.mll | |
parent | 88613c0f5415a0d3f2e0e0e9ff74bd32b6b4685e (diff) | |
download | compcert-17f519651feb4a09aa90c89c949469e8a5ab0e88.tar.gz compcert-17f519651feb4a09aa90c89c949469e8a5ab0e88.zip |
- Support "switch" statements over 64-bit integers
(in CompCert C to Cminor, included)
- Translation of "switch" to decision trees or jumptables made generic
over the sizes of integers and moved to the Cminor->CminorSel pass
instead of CminorSel->RTL as before.
- CminorSel: add "exitexpr" to support the above.
- ValueDomain: more precise analysis of comparisons against an integer
literal. E.g. "x >=u 0" is always true.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CMlexer.mll')
-rw-r--r-- | backend/CMlexer.mll | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll index d1926fda..7ed5b4ab 100644 --- a/backend/CMlexer.mll +++ b/backend/CMlexer.mll @@ -149,6 +149,7 @@ rule token = parse | "*f" { STARF } | "*l" { STARL } | "switch" { SWITCH } + | "switchl" { SWITCHL } | "tailcall" { TAILCALL } | "~" { TILDE } | "~l" { TILDEL } |