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
|
import org.checkerframework.checker.interning.qual.Interned;
class OverrideInterned {
// This code is extracted from FreePastry
@Interned class NodeHandle {}
public interface TransportLayer<IDENTIFIER> {
public void sendMessage(IDENTIFIER i);
}
public class CommonAPITransportLayerImpl<IDENTIFIER extends NodeHandle>
implements TransportLayer<IDENTIFIER> {
public void sendMessage(IDENTIFIER i) {}
}
interface MessageReceipt {
public NodeHandle getHint();
}
void useAnonymousClass() {
MessageReceipt ret =
new MessageReceipt() {
public NodeHandle getHint() {
return null;
}
};
}
// This code is from Daikon
public abstract class TwoSequenceString {
public abstract Object check_modified1(@Interned String @Interned [] v1);
public abstract Object check_modified2(String @Interned [] v1);
}
/* Changing the array component type in the overriding method is illegal. */
public class PairwiseStringEqualBad extends TwoSequenceString {
// TODOINVARR:: error: (override.param.invalid)
public Object check_modified1(String @Interned [] a1) {
return new Object();
}
// :: error: (override.param.invalid)
public Object check_modified2(@Interned String @Interned [] a1) {
return new Object();
}
}
/* Changing the main reference type is allowed, if it is a supertype. */
public class PairwiseStringEqualGood extends TwoSequenceString {
public Object check_modified1(@Interned String[] a1) {
return new Object();
}
public Object check_modified2(String[] a1) {
return new Object();
}
}
}
|
