Lazy methods: mark JVM-generated exceptions as always available#1467
Lazy methods: mark JVM-generated exceptions as always available#1467antlechner wants to merge 1 commit intodiffblue:developfrom
Conversation
java.lang.NullPointerException et al are producable from Java ops other than throw, and therefore weren't previously noticed. This adds the exceptions that can be introduced by java_bytecode/java_bytecode_instrument.cpp into the lazy methods loader's list of always-available classes.
smowton
left a comment
There was a problem hiding this comment.
I approve of course, but then I wrote it :)
LAJW
left a comment
There was a problem hiding this comment.
It would be helpful if this PR included an example of what it's fixing.
|
An example of why this PR is/will be needed: With the current platform options, the |
thk123
left a comment
There was a problem hiding this comment.
I agree with @LAJW - could you take your example and create regression or unit tests exhibiting the problem this will fix (pref ably one for each type of exception). Or if there are already tests for each exception (they're should be...), extend them to use lazy-methods and the models library so that they would catch this in future.
| lazy_methods.add_needed_class( | ||
| "java::java.lang.ArrayIndexOutOfBoundsException"); | ||
| lazy_methods.add_needed_class("java::java.lang.ClassCastException"); | ||
| lazy_methods.add_needed_class("java::java.lang.NegativeArraySizeException"); |
There was a problem hiding this comment.
Consider adding a comment to java_bytecode_instrument::instrument_expr to say that new runtime thrown exceptions need to be added to ci_lazy_methods.cpp
|
test-gen doesn't build with the version of cbmc that this is based on, so I'll rebase the changes on my fork and create a new PR. I'll close this one and link the new one here. Sorry about that. |
java.lang.NullPointerException et al are producable from Java ops
other than throw, and therefore weren't previously noticed. This adds
the exceptions that can be introduced by java_bytecode/java_bytecode_instrument.cpp
into the lazy methods loader's list of always-available classes.