File: Defaulting.java

package info (click to toggle)
checker-framework-java 3.2.0%2Bds-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 22,840 kB
  • sloc: java: 145,910; xml: 839; sh: 518; makefile: 401; perl: 26
file content (167 lines) | stat: -rw-r--r-- 5,701 bytes parent folder | download | duplicates (3)
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
import org.checkerframework.framework.qual.DefaultQualifier;
import org.checkerframework.framework.qual.TypeUseLocation;
import testchecker.quals.*;

// Test defaulting behavior, e.g. that local variables, casts, and instanceof
// propagate the type of the respective sub-expression and that upper bounds
// are separately annotated.
class Defaulting {

    @DefaultQualifier(
            value = H1S1.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    class TestLocal {
        void m(@H1S1 Object p1, @H1S2 Object p2) {
            Object l1 = p1;
            // :: error: (assignment.type.incompatible)
            Object l2 = p2;
        }
    }

    @DefaultQualifier(
            value = H1Top.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    @DefaultQualifier(
            value = H1S1.class,
            locations = {TypeUseLocation.UPPER_BOUND})
    @DefaultQualifier(
            value = H1S2.class,
            locations = {TypeUseLocation.OTHERWISE})
    // Type of x is <@H1S2 X extends @H1S1 Object>, these annotations are siblings
    // and should not be in the same bound
    // :: warning: (inconsistent.constructor.type) :: error: (bound.type.incompatible) :: error:
    // (super.invocation.invalid)
    class TestUpperBound<X extends Object> {
        void m(X p) {
            @H1S1 Object l1 = p;
            // :: error: (assignment.type.incompatible)
            @H1S2 Object l2 = p;
            Object l3 = p;
        }
    }

    @DefaultQualifier(
            value = H1Top.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    @DefaultQualifier(
            value = H1S1.class,
            locations = {TypeUseLocation.PARAMETER})
    @DefaultQualifier(
            value = H1S2.class,
            locations = {TypeUseLocation.OTHERWISE})
    // :: warning: (inconsistent.constructor.type) :: error: (super.invocation.invalid)
    class TestParameter {
        void m(Object p) {
            @H1S1 Object l1 = p;
            // :: error: (assignment.type.incompatible)
            @H1S2 Object l2 = p;
            Object l3 = p;
        }

        void call() {
            // :: warning: (cast.unsafe.constructor.invocation)
            m(new @H1S1 Object());
            // :: error: (argument.type.incompatible) :: warning:
            // (cast.unsafe.constructor.invocation)
            m(new @H1S2 Object());
            // :: error: (argument.type.incompatible)
            m(new Object());
        }
    }

    @DefaultQualifier(
            value = H1Top.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    @DefaultQualifier(
            value = H1S1.class,
            locations = {TypeUseLocation.PARAMETER})
    @DefaultQualifier(
            value = H1S2.class,
            locations = {TypeUseLocation.OTHERWISE})
    class TestConstructorParameter {

        // :: warning: (inconsistent.constructor.type) :: error: (super.invocation.invalid)
        TestConstructorParameter(Object p) {
            @H1S1 Object l1 = p;
            // :: error: (assignment.type.incompatible)
            @H1S2 Object l2 = p;
            Object l3 = p;
        }

        void call() {
            // :: warning: (cast.unsafe.constructor.invocation)
            new TestConstructorParameter(new @H1S1 Object());
            // :: error: (argument.type.incompatible) :: warning:
            // (cast.unsafe.constructor.invocation)
            new TestConstructorParameter(new @H1S2 Object());
            // :: error: (argument.type.incompatible)
            new TestConstructorParameter(new Object());
        }
    }

    @DefaultQualifier(
            value = H1Top.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    @DefaultQualifier(
            value = H1S1.class,
            locations = {TypeUseLocation.RETURN})
    @DefaultQualifier(
            value = H1S2.class,
            locations = {TypeUseLocation.OTHERWISE})
    // :: warning: (inconsistent.constructor.type) :: error: (super.invocation.invalid)
    class TestReturns {
        Object res() {
            // :: warning: (cast.unsafe.constructor.invocation)
            return new @H1S1 Object();
        }

        void m() {
            @H1S1 Object l1 = res();
            // :: error: (assignment.type.incompatible)
            @H1S2 Object l2 = res();
            Object l3 = res();
        }

        Object res2() {
            // :: error: (return.type.incompatible) :: warning: (cast.unsafe.constructor.invocation)
            return new @H1S2 Object();
        }

        Object res3() {
            // :: error: (return.type.incompatible)
            return new Object();
        }
    }

    @DefaultQualifier(
            value = H1Top.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    @DefaultQualifier(
            value = H1S1.class,
            locations = {TypeUseLocation.RECEIVER})
    public class ReceiverDefaulting {
        public ReceiverDefaulting() {};

        public void m() {}
    }

    @DefaultQualifier(
            value = H1Top.class,
            locations = {TypeUseLocation.LOCAL_VARIABLE})
    class TestReceiver {

        void call() {
            // :: warning: (cast.unsafe.constructor.invocation)
            @H1S1 ReceiverDefaulting r2 = new @H1S1 ReceiverDefaulting();
            // :: warning: (cast.unsafe.constructor.invocation)
            @H1S2 ReceiverDefaulting r3 = new @H1S2 ReceiverDefaulting();
            ReceiverDefaulting r = new ReceiverDefaulting();

            r2.m();
            // :: error: (method.invocation.invalid)
            r3.m();
            // :: error: (method.invocation.invalid)
            r.m();
        }
    }
}