Lazy methods: mark JVM-generated exceptions as always available

[antlechner]

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.

[antlechner]

Suggested reviewers:
@thk123 @smowton @LAJW

[smowton]

I approve of course, but then I wrote it :)

[LAJW]

It would be helpful if this PR included an example of what it's fixing.

[antlechner]

An example of why this PR is/will be needed:

public static int check1(String s) {
    try {
        return s.length();
    }
    catch (NullPointerException e) {
        e.getMessage();
        return -1;
    }
}

With the current platform options, the catch block is ignored. But with the --java-throw-runtime-exceptions parameter (which will be added as a platform option at some point, hopefully soon), test-gen tries to generate a test for catch block, looks up NullPointerException.getMessage, and can't find it because the exception is generated after lazy methods analysed the code. The result is an error and no generated tests.

[thk123]

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.

[thk123]

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

[antlechner]

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.