Merge pull request #3307 from smowton/smowton/fix/remove-exceptions-after-convert-nondet

JBMC: run remove_exceptions after replace_java_nondet

Author: tautschnig

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());