From 891377ce1962cdb31357d6580d6546ec22df2b4f Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:22:27 +0000 Subject: 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 --- backend/RTLgenaux.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'backend/RTLgenaux.ml') 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 -- cgit