JBMC: run remove_exceptions after replace_java_nondet

The latter can introduce functions that need exception handlers, or more usually an ASSUME(@inflight_exception == null) guard
against accidentally propagated exceptions. When replace_java_nondet is run after exception removal we can get odd behaviour,
shown by the included test case, as the exception will be detected later than it should have been, or would escape from the
ASSUME guard implied by a @MustNotThrow annotation.

Author: smowton

jbmc/regression/jbmc/nondet_initialize_exception_handler/Fake.class

@@ -0,0 +1,33 @@
+public class JavaExceptionTest {
+
+    public static Fake getFake() {
+        try {
+            return org.cprover.CProver.nondetWithoutNull((Fake)null);
+        }
+        catch(Exception t) {
+            // Should be reachable due to exception thrown in
+            // nondet-initialize:
+            return new Fake();
+        }
+    }
+
+    void test () {
+
+        Fake a = null;
+        try {
+            a = getFake();
+        }
+        catch(Exception t) {
+            // Should be unreachable
+            assert false;
+        }
+
+    }
+
+}
+
+class Fake {
+    protected final void cproverNondetInitialize() throws Exception {
+        throw new Exception("Oh dear oh dear");
+    }
+}

jbmc/regression/jbmc/nondet_initialize_exception_handler/JavaExceptionTest$Fake.class

@@ -0,0 +1,6 @@
+CORE
+JavaExceptionTest.class
+--function JavaExceptionTest.test
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$

jbmc/regression/jbmc/nondet_initialize_exception_handler/JavaExceptionTest.class

@@ -738,20 +738,6 @@ void jbmc_parse_optionst::process_goto_function(
     // Java virtual functions -> explicit dispatch tables:
     remove_virtual_functions(function);
 
-    if(using_symex_driven_loading)
-    {
-      // remove exceptions
-      // If using symex-driven function loading we need to do this now so that
-      // symex doesn't have to cope with exception-handling constructs; however
-      // the results are slightly worse than running it in whole-program mode
-      // (e.g. dead catch sites will be retained)
-      remove_exceptions(
-        goto_function.body,
-        symbol_table,
-        *class_hierarchy.get(),
-        get_message_handler());
-    }
-
     auto function_is_stub = [&symbol_table, &model](const irep_idt &id) {
       return symbol_table.lookup_ref(id).value.is_nil() &&
              !model.can_produce_function(id);
@@ -768,6 +754,20 @@ void jbmc_parse_optionst::process_goto_function(
       object_factory_params,
       ID_java);
 
+    if(using_symex_driven_loading)
+    {
+      // remove exceptions
+      // If using symex-driven function loading we need to do this now so that
+      // symex doesn't have to cope with exception-handling constructs; however
+      // the results are slightly worse than running it in whole-program mode
+      // (e.g. dead catch sites will be retained)
+      remove_exceptions(
+        goto_function.body,
+        symbol_table,
+        *class_hierarchy.get(),
+        get_message_handler());
+    }
+
     // add generic checks
     goto_check(ns, options, ID_java, function.get_goto_function());