We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent d299ea2 commit 82642b9Copy full SHA for 82642b9
regression/cbmc-java/exceptions20/A.class
234 Bytes
regression/cbmc-java/exceptions20/B.class
216 Bytes
regression/cbmc-java/exceptions20/C.class
regression/cbmc-java/exceptions20/D.class
regression/cbmc-java/exceptions20/test.class
1 KB
regression/cbmc-java/exceptions20/test.desc
@@ -0,0 +1,11 @@
1
+CORE
2
+test.class
3
+--json-ui --trace
4
+^EXIT=10$
5
+^SIGNAL=0$
6
+.*VERIFICATION FAILED.*
7
+--
8
+^warning: ignoring
9
10
+this fails with assertion error if nil values are not allowed in assignments in
11
+the JSON trace
regression/cbmc-java/exceptions20/test.java
@@ -0,0 +1,30 @@
+class A extends Throwable {}
+class B extends A {}
+class C extends B {}
+class D extends C {}
+
+public class test {
+ public static void main (String arg[]) {
+ try {
+ D d = new D();
+ C c = new C();
+ B b = new B();
12
+ A a = new A();
13
+ A e = a;
14
+ throw e;
15
+ }
16
+ catch(D exc) {
17
+ assert false;
18
19
+ catch(C exc) {
20
21
22
+ catch(B exc) {
23
24
25
+ catch(A exc) {
26
27
28
29
+}
30
0 commit comments