Skip to content

Java exception handling #506

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 14 commits into from
Mar 11, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file modified regression/cbmc-java/NullPointer3/NullPointer3.class
Binary file not shown.
1 change: 0 additions & 1 deletion regression/cbmc-java/NullPointer3/NullPointer3.java
Original file line number Diff line number Diff line change
Expand Up @@ -4,5 +4,4 @@ public static void main(String[] args)
{
throw null; // NULL pointer dereference
}

}
4 changes: 2 additions & 2 deletions regression/cbmc-java/NullPointer3/test.desc
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
CORE
NullPointer3.class
--pointer-check --stop-on-fail
--pointer-check
^EXIT=10$
^SIGNAL=0$
^ file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$
^.*Throw null: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
Binary file added regression/cbmc-java/exceptions1/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions1/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions1/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions1/D.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions1/test.class
Binary file not shown.
10 changes: 10 additions & 0 deletions regression/cbmc-java/exceptions1/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 26 function.*: FAILURE$
\*\* 1 of 9 failed \(2 iterations\)$
^VERIFICATION FAILED$
--
^warning: ignoring
30 changes: 30 additions & 0 deletions regression/cbmc-java/exceptions1/test.java
Original file line number Diff line number Diff line change
@@ -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();
A a = new A();
A e = a;
throw e;
}
catch(D exc) {
assert false;
}
catch(C exc) {
assert false;
}
catch(B exc) {
assert false;
}
catch(A exc) {
assert false;
}
}
}

Binary file added regression/cbmc-java/exceptions10/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions10/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions10/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions10/test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/cbmc-java/exceptions10/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 12 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
25 changes: 25 additions & 0 deletions regression/cbmc-java/exceptions10/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
class A extends RuntimeException {}
class B extends A {}
class C extends B {}

public class test {
static void foo() {
try {
A b = new A();
throw b;
}
catch(A exc) {
assert false;
}
}

public static void main (String args[]) {
try {
A a = new A();
foo();
}
catch(B exc) {
assert false;
}
}
}
Binary file added regression/cbmc-java/exceptions11/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions11/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions11/test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/cbmc-java/exceptions11/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 36 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
39 changes: 39 additions & 0 deletions regression/cbmc-java/exceptions11/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
class A extends RuntimeException {
int i=1;
};

class B extends A {
};

public class test {
static int foo(int k) {
try {
if(k==0)
{
A a = new A();
throw a;
}
else
{
A b = new A();
throw b;
}

}
catch(B exc) {
assert exc.i==1;
}
return 1;
}


public static void main (String args[]) {
try {
A a = new A();
foo(6);
}
catch(A exc) {
assert exc.i==2;
}
}
}
Binary file added regression/cbmc-java/exceptions12/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions12/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions12/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions12/F.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions12/test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/cbmc-java/exceptions12/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 12 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
27 changes: 27 additions & 0 deletions regression/cbmc-java/exceptions12/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
class A extends RuntimeException {}
class B extends A {}
class C extends B {}

class F {
void foo() {
try {
B b = new B();
throw b;
}
catch(B exc) {
assert false;
}
}
}

public class test {
public static void main (String args[]) {
try {
F f = new F();
f.foo();
}
catch(B exc) {
assert false;
}
}
}
Binary file added regression/cbmc-java/exceptions13/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions13/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions13/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions13/F.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions13/test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/cbmc-java/exceptions13/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 25 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
28 changes: 28 additions & 0 deletions regression/cbmc-java/exceptions13/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
class A extends RuntimeException {}
class B extends A {}
class C extends B {}

class F {
void foo() {
try {
B b = new B();
throw b;
}
catch(B exc) {
throw exc;
}
}
}

public class test {

public static void main (String args[]) {
try {
F f = new F();
f.foo();
}
catch(B exc) {
assert false;
}
}
}
Binary file added regression/cbmc-java/exceptions14/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions14/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions14/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions14/test.class
Binary file not shown.
8 changes: 8 additions & 0 deletions regression/cbmc-java/exceptions14/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
test.class

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
24 changes: 24 additions & 0 deletions regression/cbmc-java/exceptions14/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
class A extends RuntimeException {}
class B extends A {}
class C extends B {}

public class test {
public static void main (String args[]) {
try {
try {
C c = new C();
A a = new A();
}
catch(C exc) {
assert false;
}
catch(B exc) {
assert false;
}
}
catch(A exc) {
assert false;
}

}
}
Binary file added regression/cbmc-java/exceptions15/InetAddress.class
Binary file not shown.
Binary file not shown.
Binary file added regression/cbmc-java/exceptions15/test.class
Binary file not shown.
8 changes: 8 additions & 0 deletions regression/cbmc-java/exceptions15/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
test.class
--function test.translate
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
20 changes: 20 additions & 0 deletions regression/cbmc-java/exceptions15/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
class InetAddress {}
class InetSocketAddress {}

public class test {
public String lookupPtrRecord(InetAddress address) {
return "Foo";
}

public InetAddress reverse(InetAddress address) {
return address;
}

public void translate(InetAddress address, int i) {
try {
String domainName = lookupPtrRecord(reverse(address));
} catch (Exception e) {
assert false;
}
}
}
Binary file added regression/cbmc-java/exceptions16/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions16/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions16/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions16/test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/cbmc-java/exceptions16/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
test.class
--function test.foo
^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 18 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
21 changes: 21 additions & 0 deletions regression/cbmc-java/exceptions16/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
class A extends RuntimeException {}
class B extends A {}
class C extends B {}

public class test {
static void foo (int x) {
try {
x++;
}
catch(A exc) {
assert false;
}

try {
throw new B();
}
catch(B exc) {
assert false;
}
}
}
Binary file added regression/cbmc-java/exceptions18/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions18/Test.class
Binary file not shown.
23 changes: 23 additions & 0 deletions regression/cbmc-java/exceptions18/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
class A extends RuntimeException {}
class B extends A {}

public class Test {
void foo()
{
A a=new A();
throw a;
}
void goo()
{
try
{
foo();
assert false;
}
catch(B e)
{
assert false;
}
}

}
8 changes: 8 additions & 0 deletions regression/cbmc-java/exceptions18/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
Test.class
--function Test.goo
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
Binary file added regression/cbmc-java/exceptions2/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions2/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions2/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions2/test.class
Binary file not shown.
10 changes: 10 additions & 0 deletions regression/cbmc-java/exceptions2/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 15 function.*: FAILURE$
^\*\* 1 of 5 failed \(2 iterations\)$
^VERIFICATION FAILED$
--
^warning: ignoring
18 changes: 18 additions & 0 deletions regression/cbmc-java/exceptions2/test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
class A extends Throwable {}
class B extends A {}
class C extends B {}

public class test {
public static void main (String args[]) {
try {
B b = new B();
throw b;
}
catch(C exc) {
assert false;
}
catch(B exc) {
assert false;
}
}
}
Binary file added regression/cbmc-java/exceptions3/A.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions3/B.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions3/C.class
Binary file not shown.
Binary file added regression/cbmc-java/exceptions3/test.class
Binary file not shown.
9 changes: 9 additions & 0 deletions regression/cbmc-java/exceptions3/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
test.class

^EXIT=10$
^SIGNAL=0$
^.*assertion at file test.java line 14 function.*: FAILURE$
^VERIFICATION FAILED$
--
^warning: ignoring
Loading