1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
import org.checkerframework.checker.fenum.qual.SwingHorizontalOrientation;
import org.checkerframework.checker.fenum.qual.SwingVerticalOrientation;
public class FlowBreak {
static @SwingHorizontalOrientation Object CENTER;
static @SwingHorizontalOrientation Object LEFT;
boolean flag;
@SwingHorizontalOrientation Object testInference() {
Object o;
// initially o is @FenumTop
o = null;
// o is @Bottom
while (flag) {
if (flag) {
o = CENTER;
// o is @SwingHorizontalOrientation
} else {
o = new @SwingVerticalOrientation Object();
// o is @SwingVerticalOrientation
break;
}
// We can only come here from the then-branch, the else-branch is dead.
// Therefore, we only take the annotations at the end of
// the then-branch and ignore the results of the else-branch.
// Therefore, o is @SwingHorizontalOrientation and the
// following is valid:
@SwingHorizontalOrientation Object pla = o;
}
// Here we have to merge three paths:
// 1. The entry to the loop, if the condition is false [@Bottom]
// 2. The normal end of the loop body [@SwingHorizontalOrientation]
// 3. The path from the break to here [@SwingVerticalOrientation]
// Currently, the third path is ignored and we do not get this error message.
// :: error: (return.type.incompatible)
return o;
}
}
|
