diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-21 20:29:57 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-21 20:29:57 +0100 |
| commit | 47a4ccade6f73e95be34cd2d55be3655302fff97 (patch) | |
| tree | c2369513d83bf3a5a7872dce60e20926de8e76f0 /common/Switchaux.ml | |
| parent | ab5528fb4caf637a0c7014d943302198079e7c20 (diff) | |
| download | compcert-kvx-47a4ccade6f73e95be34cd2d55be3655302fff97.tar.gz compcert-kvx-47a4ccade6f73e95be34cd2d55be3655302fff97.zip | |
begin jumptables (does not work)
Diffstat (limited to 'common/Switchaux.ml')
| -rw-r--r-- | common/Switchaux.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 06337e7d..69300feb 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -80,10 +80,6 @@ let compile_switch_as_jumptable default cases minkey maxkey = CTaction default) let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = - (* FIXME DMonniaux disable jump tables until we can prove them through *) - false - -(* let span = Z.sub maxkey minkey in assert (Z.ge span Z.zero); let tree_size = Z.mul (Z.of_uint 4) (Z.of_uint numcases) @@ -91,7 +87,6 @@ let dense_enough (numcases: int) (minkey: Z.t) (maxkey: Z.t) = numcases >= 7 (* small jump tables are always less efficient *) && Z.le table_size tree_size && Z.lt span (Z.of_uint Sys.max_array_length) - *) let compile_switch modulus default table = let (tbl, keys) = normalize_table table in |