-
Notifications
You must be signed in to change notification settings - Fork 14
Description
ocamljava fails with
"Error: Cannot compile goto_table_4081 (Java method is too long: 94429 bytes)"
The function in question is generated by Menhir into Coq, then extracted into OCaml, so I really have no way to make this function shorter.
I believe JVM methods are not limited to 65535 bytes in code length; only exception handlers are. See http://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.7.3
code_length is a 32-bit integer. It's only the _pc fields of exception_table entries that are 16 bits. ("A historical mistake in the design" as the spec calls it.) In the Java standard library, you'll find several static class initialization methods that are > 64K in code length.
Would it be possible for ocamljava to emit this error only if there is an exception handler that overflows the first 64K of JVM code? This would fix my problem nicely, since the big function in question has no exception handlers, like all functions generated by Coq extraction.