Skip to content

Commit 706ffa7

Browse files
committed
Make test lambda1 compatible with symex-driven loading
Previously it didn't have an entry-point, and so relied on the normal load process loading all functions. The added entry-point mimics that behaviour when loading is on-demand.
1 parent 3b00bdc commit 706ffa7

File tree

6 files changed

+21
-3
lines changed

6 files changed

+21
-3
lines changed

regression/cbmc-java/lambda1/B.class

-123 Bytes
Binary file not shown.

regression/cbmc-java/lambda1/C.class

-124 Bytes
Binary file not shown.
-73 Bytes
Binary file not shown.
-767 Bytes
Binary file not shown.

regression/cbmc-java/lambda1/Lambdatest.java

Lines changed: 15 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,11 @@ public int j(int x) {
3636

3737
public int k(int x) {
3838
a.x = 10;
39-
39+
4040
Function<Integer, Integer> foo = (y) -> y * a.x;
4141
return foo.apply(x);
4242
}
43-
43+
4444
public int l(int x) {
4545
b.y = 10;
4646
Function<Integer, Integer> foo = (y) -> {
@@ -75,6 +75,19 @@ public int capture2(Float a) {
7575
public boolean custom(Integer i) {
7676
return custom.is_ok(i);
7777
}
78+
79+
public static void main(String[] args) {
80+
// Uses all of the above test functions, to ensure they are loaded under
81+
// symex-driven loading:
82+
83+
Lambdatest lt = new Lambdatest();
84+
lt.f(0.0f, 0, 0);
85+
lt.i(0);
86+
lt.j(0);
87+
lt.k(0);
88+
lt.l(0);
89+
lt.m(0);
90+
}
7891
}
7992

8093
class C implements CustomLambda<Integer> {

regression/cbmc-java/lambda1/test.desc

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
Lambdatest.class
3-
--verbosity 10 --show-goto-functions
3+
--verbosity 10 --show-goto-functions --function Lambdatest.main
44
lambda function reference lambda\$new\$0 in class \"Lambdatest\"
55
lambda function reference lambda\$new\$1 in class \"Lambdatest\"
66
lambda function reference lambda\$f\$2 in class \"Lambdatest\"
@@ -12,3 +12,8 @@ lambda function reference lambda\$m\$7 in class \"Lambdatest\"
1212
lambda function reference lambda\$static\$0 in class \"B\"
1313
^EXIT=0$
1414
^SIGNAL=0$
15+
--
16+
--
17+
Incompatible with symex-driven lazy loading because this test wants to process
18+
everything in the given class, not the functions reachable from a particular
19+
entry point, which is required for symex-driven loading.

0 commit comments

Comments
 (0)