Skip to content

Commit a718893

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 20645c9 commit a718893

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)