diff options
| -rw-r--r-- | common/Switchaux.ml | 7 | ||||
| -rw-r--r-- | test/monniaux/jpeg-6b/jconfig.h | 2 |
2 files changed, 7 insertions, 2 deletions
diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 4035e299..06337e7d 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -80,6 +80,10 @@ 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) @@ -87,7 +91,8 @@ 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 if ZSet.is_empty keys then CTaction default else begin diff --git a/test/monniaux/jpeg-6b/jconfig.h b/test/monniaux/jpeg-6b/jconfig.h index b2f0b94f..1c6bd8af 100644 --- a/test/monniaux/jpeg-6b/jconfig.h +++ b/test/monniaux/jpeg-6b/jconfig.h @@ -28,7 +28,7 @@ */ #define HAVE_PROTOTYPES -#define NO_SWITCH +#undef NO_SWITCH #ifdef __COMPCERT__ extern long long __compcert_i64_sdiv(long long a, long long b); |