Skip to content

Commit 8888c0e

Browse files
author
thk123
committed
Adding test to ensure methods on return type of opaque function
These methods should be loaded for all classes where an instance might be seen and the return of an opaque method is one such instance.
1 parent 293ceff commit 8888c0e

File tree

14 files changed

+56
-0
lines changed

14 files changed

+56
-0
lines changed
333 Bytes
Binary file not shown.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
public class Bar {
2+
public int x;
3+
4+
public void cproverNondetInitialize() {
5+
6+
}
7+
}
317 Bytes
Binary file not shown.
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
public class Baz {
2+
public void cproverNondetInitialize() {
3+
4+
}
5+
}
445 Bytes
Binary file not shown.
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Foo {
2+
public Bar subType;
3+
4+
public Baz[] arraySubtype;
5+
6+
public Gen<GenFiller> genSubtype;
7+
8+
public void cproverNondetInitialize() {
9+
10+
}
11+
}
400 Bytes
Binary file not shown.
Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
public class Gen<T> {
2+
T t;
3+
}
351 Bytes
Binary file not shown.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
public class GenFiller {
2+
public int i;
3+
4+
public void cproverNondetInitialize() {
5+
6+
}
7+

0 commit comments

Comments
 (0)