Assert that there is uncaught exception

An uncaught exception makes the JVM abort.
That's the default error behaviour the JBMC should check.

Author: peterschrammel

regression/cbmc-java/exceptions18/test.desc

@@ -1,8 +1,9 @@
 CORE
 Test.class
 --function Test.goo
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
+no uncaught exception: FAILURE
 --
 ^warning: ignoring

src/java_bytecode/java_entry_point.cpp

@@ -294,6 +294,16 @@ void java_record_outputs(
   output.add_source_location()=function.location;
 
   init_code.move_to_operands(output);
+
+  // check that there is no uncaught exception
+  code_assertt assert_no_exception;
+  assert_no_exception.assertion() =
+    equal_exprt(exc_symbol.symbol_expr(),
+                null_pointer_exprt(to_pointer_type(exc_symbol.type)));
+  source_locationt assert_location = function.location;
+  assert_location.set_comment("no uncaught exception");
+  assert_no_exception.add_source_location() = assert_location;
+  init_code.move_to_operands(assert_no_exception);
 }
 
 main_function_resultt get_main_symbol(