Skip to content

Commit 102fe5c

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 21eaccb commit 102fe5c

File tree

14 files changed

+56
-0
lines changed

14 files changed

+56
-0
lines changed
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+
}
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+
}
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+
}
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+
}
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)