Fix nonsensical jbmc/catch1 test

some_exception1 and some_exception2 classes were missing,
leading to wrong results.
Changed to test to check in heritance behavior on
catching exception classes.

Author: peterschrammel

jbmc/regression/jbmc/catch1/src/main/java/catch1.java

@@ -8,7 +8,7 @@ class some_exception2 extends some_exception1
 
 class catch1
 {
-  public static void main(String[] args)
+  public static void catchSuper() throws Throwable
   {
     try
     {
@@ -19,5 +19,17 @@ public static void main(String[] args)
     {
     }
   }
+
+  public static void catchSub() throws Throwable
+  {
+    try
+    {
+      throw new some_exception1();
+    }
+
+    catch(some_exception2 e)
+    {
+    }
+  }
 }
 

jbmc/regression/jbmc/catch1/test.desc renamed to jbmc/regression/jbmc/catch1/test_catch_sub.desc

@@ -1,9 +1,9 @@
 CORE
-catch1
+catch1.catchSub
 -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\[.*\] line 15 no uncaught exception: FAILURE$
+^\[.*\] line 27 no uncaught exception: FAILURE$
 --
 ^warning: ignoring

jbmc/regression/jbmc/catch1/test_no_uncaught_exceptions.desc renamed to jbmc/regression/jbmc/catch1/test_catch_super.desc

@@ -1,6 +1,6 @@
 CORE
-catch1
---disable-uncaught-exception-check -cp target/classes
+catch1.catchSuper
+-cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$