Skip to content

Commit c1a2f4d

Browse files
Lukasz A.J. Wronasmowton
Lukasz A.J. Wrona
authored and
smowton
committed
Formatting
1 parent bd8f557 commit c1a2f4d

18 files changed

+88
-110
lines changed

‎jbmc/regression/jbmc/lambda-unhandled-types/InterfaceDeclaringEquals.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,4 @@ interface InterfaceDeclaringEquals {
33
public int f(int x);
44

55
public boolean equals(Object other);
6-
76
}

‎jbmc/regression/jbmc/lambda-unhandled-types/InterfaceWithDefaults.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,4 @@ interface InterfaceWithDefaults {
33
public int f(int x);
44

55
public default int g() { return 1; }
6-
76
}

‎jbmc/regression/jbmc/lambda-unhandled-types/StubInterface.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
interface StubInterface {
22

33
public int f(int x);
4-
54
}

‎jbmc/regression/jbmc/lambda-unhandled-types/StubSuperinterface.java

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1 @@
1-
interface StubSuperinterface extends StubInterface {
2-
3-
}
1+
interface StubSuperinterface extends StubInterface {}

‎jbmc/regression/jbmc/lambda-unhandled-types/Test.java

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,5 @@ public static void main() {
66
StubSuperinterface stubSuperinterface = (x -> x);
77
InterfaceDeclaringEquals interfaceDeclaringEquals = (x -> x);
88
InterfaceWithDefaults interfaceWithDefaults = (x -> x);
9-
109
}
11-
1210
}

‎jbmc/regression/jbmc/lambda1/B.class

-4 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/lambda1/B.java

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
public class B {
2-
public int y;
2+
public int y;
33

4-
public static Function<Double, Double> dmul = x -> x * 1.5;
4+
public static Function<Double, Double> dmul = x -> x * 1.5;
55

6-
public void set(int x) {
7-
y = x;
8-
}
6+
public void set(int x) { y = x; }
97
}

‎jbmc/regression/jbmc/lambda1/BiFunction.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,4 @@
22
interface BiFunction<From1, From2, To> {
33

44
public To apply(From1 f1, From2 f2);
5-
65
}

‎jbmc/regression/jbmc/lambda1/C.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/lambda1/CustomLambda.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
@FunctionalInterface
22
interface CustomLambda<T> {
3-
boolean is_ok(T t);
3+
boolean is_ok(T t);
44
}

‎jbmc/regression/jbmc/lambda1/Function.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,4 @@
22
interface Function<From, To> {
33

44
public To apply(From f);
5-
65
}

‎jbmc/regression/jbmc/lambda1/Lambdatest.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/lambda1/Lambdatest.java

Lines changed: 52 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ class A {
1111
A a = new A();
1212
B b = new B();
1313

14-
public Integer captureNone(Float x, Integer y, BiFunction<Float, Integer, Integer> fun) {
14+
public Integer captureNone(Float x, Integer y,
15+
BiFunction<Float, Integer, Integer> fun) {
1516
return fun.apply(x, y);
1617
}
1718

@@ -62,111 +63,103 @@ public int captureAndAssign(int x) {
6263
}
6364

6465
// test static field of different class
65-
public double callStatic(Double x) {
66-
return B.dmul.apply(x);
67-
}
66+
public double callStatic(Double x) { return B.dmul.apply(x); }
6867

69-
public int capture2(Float a) {
70-
return add.apply(a, 1);
71-
}
68+
public int capture2(Float a) { return add.apply(a, 1); }
7269

73-
public boolean custom(Integer i) {
74-
return custom.is_ok(i);
75-
}
70+
public boolean custom(Integer i) { return custom.is_ok(i); }
7671

7772
public static void main(String[] args, int unknown) {
7873
Lambdatest lt = new Lambdatest();
79-
if(unknown == 0)
80-
assert lt.captureNone(1.0f, 2, (x, y) -> x.intValue() + y) == 3; // should succeed
81-
else if(unknown == 1)
82-
assert lt.captureNone(1.0f, 2, (x, y) -> x.intValue() + y) == 4; // should fail
83-
else if(unknown == 2)
74+
if (unknown == 0) {
75+
// should succeed
76+
assert lt.captureNone(1.0f, 2, (x, y) -> x.intValue() + y) == 3;
77+
} else if (unknown == 1) {
78+
// should fail
79+
assert lt.captureNone(1.0f, 2, (x, y) -> x.intValue() + y) == 4;
80+
} else if (unknown == 2) {
8481
assert lt.captureReference(1.0f, 2, 3) == 9; // should succeed
85-
else if(unknown == 3)
82+
} else if (unknown == 3) {
8683
assert lt.captureReference(1.0f, 2, 3) == 10; // should fail
87-
else if(unknown == 4)
84+
} else if (unknown == 4) {
8885
assert lt.captureInt(2) == 10; // should succeed
89-
else if(unknown == 5)
86+
} else if (unknown == 5) {
9087
assert lt.captureInt(2) == 11; // should fail
91-
else if(unknown == 6)
88+
} else if (unknown == 6) {
9289
assert lt.captureThisPrimitive(3) == 30; // should succeed
93-
else if(unknown == 7)
90+
} else if (unknown == 7) {
9491
assert lt.captureThisPrimitive(3) == 31; // should fail
95-
else if(unknown == 8)
92+
} else if (unknown == 8) {
9693
assert lt.captureThisReference(4) == 40; // should succeed
97-
else if(unknown == 9)
94+
} else if (unknown == 9) {
9895
assert lt.captureThisReference(4) == 41; // should fail
99-
else if(unknown == 10)
100-
{
96+
} else if (unknown == 10) {
10197
assert lt.captureAndCall(5) == 70; // should succeed
102-
assert lt.b.y == 70; // check side-effects of l method
103-
}
104-
else if(unknown == 11)
98+
assert lt.b.y == 70; // check side-effects of l method
99+
} else if (unknown == 11) {
105100
assert lt.captureAndCall(5) == 51; // should fail
106-
else if(unknown == 12)
107-
{
101+
} else if (unknown == 12) {
108102
assert lt.captureAndAssign(6) == 60; // should succeed
109-
assert lt.b.y == 60; // check side-effects of m method
110-
}
111-
else if(unknown == 13)
103+
assert lt.b.y == 60; // check side-effects of m method
104+
} else if (unknown == 13) {
112105
assert lt.captureAndAssign(6) == 61; // should fail
113-
else if(unknown == 14)
106+
} else if (unknown == 14) {
114107
assert lt.callStatic(7.0) == 10.5; // should succeed
115-
else if(unknown == 15)
108+
} else if (unknown == 15) {
116109
assert lt.callStatic(7.0) == 12; // should fail
117-
else if(unknown == 16)
110+
} else if (unknown == 16) {
118111
assert lt.capture2(8.0f) == 9; // should succeed
119-
else if(unknown == 17)
112+
} else if (unknown == 17) {
120113
assert lt.capture2(8.0f) == 10; // should fail
121-
else if(unknown == 18)
114+
} else if (unknown == 18) {
122115
assert lt.custom(9); // should succeed
123-
else if(unknown == 19)
116+
} else if (unknown == 19) {
124117
assert !lt.custom(9); // should fail
125-
// Test array capture
126-
else if(unknown == 20) {
118+
// Test array capture
119+
} else if (unknown == 20) {
127120
int array[] = new int[3];
128121
Function<Integer, Integer> func = (x) -> x + array.length;
129122
assert func.apply(2) == 5; // should succeed
130-
} else if(unknown == 21) {
123+
} else if (unknown == 21) {
131124
int array[] = new int[3];
132125
Function<Integer, Integer> func = (x) -> x + array.length;
133126
assert func.apply(2) == 6; // should fail
134-
// Test reference array
135-
} else if(unknown == 22) {
127+
// Test reference array
128+
} else if (unknown == 22) {
136129
Integer array[] = new Integer[3];
137130
Function<Integer, Integer> func = (x) -> x + array.length;
138131
assert func.apply(2) == 5; // should succeed
139-
} else if(unknown == 23) {
132+
} else if (unknown == 23) {
140133
Integer array[] = new Integer[3];
141134
Function<Integer, Integer> func = (x) -> x + array.length;
142135
assert func.apply(2) == 6; // should fail
143-
// Test outer class capture
144-
} else if(unknown == 24) {
136+
// Test outer class capture
137+
} else if (unknown == 24) {
145138
Outer outer = new Outer();
146139
outer.value = 42;
147140
Outer.Inner inner = outer.new Inner();
148141
Function<Integer, Integer> getter = inner.getOuterGetter();
149-
assert(getter.apply(0) == 42); // should succeed
150-
} else if(unknown == 25) {
142+
assert (getter.apply(0) == 42); // should succeed
143+
} else if (unknown == 25) {
151144
Outer outer = new Outer();
152145
outer.value = 42;
153146
Outer.Inner inner = outer.new Inner();
154147
Function<Integer, Integer> getter = inner.getOuterGetter();
155-
assert(getter.apply(0) != 42); // should fail
156-
// Static intialized lambda
157-
} else if(unknown == 26) {
148+
assert (getter.apply(0) != 42); // should fail
149+
// Static intialized lambda
150+
} else if (unknown == 26) {
158151
assert StaticLambdas.id.apply(96) == 96; // should succeed
159-
} else if(unknown == 27) {
152+
} else if (unknown == 27) {
160153
assert StaticLambdas.id.apply(96) != 96; // should fail
161-
// Reference equality of the captured object
162-
} else if(unknown == 28) {
154+
// Reference equality of the captured object
155+
} else if (unknown == 28) {
163156
Object object = new Object();
164157
Function<Integer, Object> lambda = (x) -> object;
165-
assert(lambda.apply(0) == object); // should succeed
166-
} else if(unknown == 29) {
158+
assert (lambda.apply(0) == object); // should succeed
159+
} else if (unknown == 29) {
167160
Object object = new Object();
168161
Function<Integer, Object> lambda = (x) -> object;
169-
assert(lambda.apply(0) != object); // should fail
162+
assert (lambda.apply(0) != object); // should fail
170163
}
171164
}
172165

@@ -183,14 +176,10 @@ class StaticLambdas {
183176
class Outer {
184177
int value;
185178
class Inner {
186-
Function<Integer, Integer> getOuterGetter() {
187-
return (x) -> value;
188-
}
179+
Function<Integer, Integer> getOuterGetter() { return (x) -> value; }
189180
}
190181
}
191182

192183
class C implements CustomLambda<Integer> {
193-
public boolean is_ok(Integer i) {
194-
return true;
195-
}
184+
public boolean is_ok(Integer i) { return true; }
196185
}

‎jbmc/regression/jbmc/lambda1/Nondet.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ public class Nondet {
33
int y;
44
public static void test(Nondet nondet) {
55
Function<Integer, Integer> lambda = (z) -> nondet.x + nondet.y + z;
6-
assert(lambda.apply(0) == 42);
6+
assert (lambda.apply(0) == 42);
77
}
88
public static void testPrimitiveArray(int[] ints) {
99
Function<Integer, Integer> lambda = (index) -> ints[index];
10-
assert(lambda.apply(0) == 42);
10+
assert (lambda.apply(0) == 42);
1111
}
1212
public static void testReferenceArray(Nondet[] nondets) {
1313
Function<Integer, Integer> lambda = (index) -> nondets[index].x;
14-
assert(lambda.apply(0) == 42);
14+
assert (lambda.apply(0) == 42);
1515
}
1616
}

‎jbmc/regression/jbmc/lambda1/Outer$Inner.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/lambda1/Outer.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/lambda1/StaticLambdas.class

0 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/lambda1/test.desc

Lines changed: 28 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,37 @@
11
CORE
22
Lambdatest.class
33
--function Lambdatest.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
4-
line 80 assertion.*SUCCESS$
5-
line 82 assertion.*FAILURE$
6-
line 84 assertion.*SUCCESS$
7-
line 86 assertion.*FAILURE$
8-
line 88 assertion.*SUCCESS$
9-
line 90 assertion.*FAILURE$
10-
line 92 assertion.*SUCCESS$
11-
line 94 assertion.*FAILURE$
12-
line 96 assertion.*SUCCESS$
13-
line 98 assertion.*FAILURE$
14-
line 101 assertion.*SUCCESS$
4+
line 76 assertion.*SUCCESS$
5+
line 79 assertion.*FAILURE$
6+
line 81 assertion.*SUCCESS$
7+
line 83 assertion.*FAILURE$
8+
line 85 assertion.*SUCCESS$
9+
line 87 assertion.*FAILURE$
10+
line 89 assertion.*SUCCESS$
11+
line 91 assertion.*FAILURE$
12+
line 93 assertion.*SUCCESS$
13+
line 95 assertion.*FAILURE$
14+
line 97 assertion.*SUCCESS$
15+
line 98 assertion.*SUCCESS$
16+
line 100 assertion.*FAILURE$
1517
line 102 assertion.*SUCCESS$
18+
line 103 assertion.*SUCCESS$
1619
line 105 assertion.*FAILURE$
17-
line 108 assertion.*SUCCESS$
18-
line 109 assertion.*SUCCESS$
19-
line 112 assertion.*FAILURE$
20-
line 114 assertion.*SUCCESS$
21-
line 116 assertion.*FAILURE$
22-
line 118 assertion.*SUCCESS$
23-
line 120 assertion.*FAILURE$
20+
line 107 assertion.*SUCCESS$
21+
line 109 assertion.*FAILURE$
22+
line 111 assertion.*SUCCESS$
23+
line 113 assertion.*FAILURE$
24+
line 115 assertion.*SUCCESS$
25+
line 117 assertion.*FAILURE$
2426
line 122 assertion.*SUCCESS$
25-
line 124 assertion.*FAILURE$
26-
line 129 assertion.*SUCCESS$
27-
line 133 assertion.*FAILURE$
28-
line 138 assertion.*SUCCESS$
29-
line 142 assertion.*FAILURE$
30-
line 149 assertion.*SUCCESS$
31-
line 155 assertion.*FAILURE$
27+
line 126 assertion.*FAILURE$
28+
line 131 assertion.*SUCCESS$
29+
line 135 assertion.*FAILURE$
30+
line 142 assertion.*SUCCESS$
31+
line 148 assertion.*FAILURE$
32+
line 151 assertion.*SUCCESS$
33+
line 153 assertion.*FAILURE$
3234
line 158 assertion.*SUCCESS$
33-
line 160 assertion.*FAILURE$
34-
line 165 assertion.*SUCCESS$
35-
line 169 assertion.*FAILURE$
35+
line 162 assertion.*FAILURE$
3636
^EXIT=10$
3737
^SIGNAL=0$

0 commit comments

Comments
 (0)