diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:22:27 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:22:27 +0000 |
| commit | 891377ce1962cdb31357d6580d6546ec22df2b4f (patch) | |
| tree | 4ff7c38749cc7a4c1af411c5aa3eb7225c4ae6a1 /backend/RTLgenaux.ml | |
| parent | 018edf2d81bf94197892cf1df221f7eeac1f96f6 (diff) | |
| download | compcert-kvx-891377ce1962cdb31357d6580d6546ec22df2b4f.tar.gz compcert-kvx-891377ce1962cdb31357d6580d6546ec22df2b4f.zip | |
Switching to the new C parser/elaborator/simplifier
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/RTLgenaux.ml')
| -rw-r--r-- | backend/RTLgenaux.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml index 1f457f3e..82cb300f 100644 --- a/backend/RTLgenaux.ml +++ b/backend/RTLgenaux.ml @@ -99,8 +99,10 @@ let dense_enough (numcases: int) (minkey: int64) (maxkey: int64) = let compile_switch default table = let (tbl, keys) = normalize_table table in - let minkey = uint64_of_coqint (IntSet.min_elt keys) - and maxkey = uint64_of_coqint (IntSet.max_elt keys) in - if dense_enough (List.length tbl) minkey maxkey - then compile_switch_as_jumptable default tbl minkey maxkey - else compile_switch_as_tree default tbl + if IntSet.is_empty keys then CTaction default else begin + let minkey = uint64_of_coqint (IntSet.min_elt keys) + and maxkey = uint64_of_coqint (IntSet.max_elt keys) in + if dense_enough (List.length tbl) minkey maxkey + then compile_switch_as_jumptable default tbl minkey maxkey + else compile_switch_as_tree default tbl + end |