File tree Expand file tree Collapse file tree 4 files changed +34
-0
lines changed
jbmc/regression/jbmc/exceptions28 Expand file tree Collapse file tree 4 files changed +34
-0
lines changed Original file line number Diff line number Diff line change
1
+ KNOWNBUG
2
+ test.class
3
+ --unwind 10
4
+ ^\[java::test.main:\(\[Ljava/lang/String;\)V\.1\] line 7 no uncaught exception: FAILURE$
5
+ ^VERIFICATION FAILED$
6
+ ^EXIT=10$
7
+ ^SIGNAL=0$
8
+ --
9
+ ^warning: ignoring
10
+ --
11
+ This test verifies that we can handle the exception table not being ordered
12
+ test.main gives the following exception table:
13
+ from to target type
14
+ 0 6 15 Class MyException
15
+ 7 15 15 Class MyException
16
+ 0 6 18 Class java/lang/Exception
17
+ 7 15 18 Class java/lang/Exception
18
+ This is not ordered in the sense that the two handlers for the block 0-6 are not next to each other.
Original file line number Diff line number Diff line change
1
+ class MyException extends Exception {}
2
+
3
+ // This test verifies that we can handle the exception table not being ordered
4
+ public class test {
5
+ public static void main (String args []) throws Exception {
6
+ try {
7
+ if (args .length == 1 )
8
+ return ;
9
+ throw new Exception ();
10
+ } catch (MyException ex ) {
11
+ throw ex ;
12
+ } catch (Exception ex ) {
13
+ throw ex ;
14
+ }
15
+ }
16
+ }
You can’t perform that action at this time.
0 commit comments