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
|
import org.checkerframework.checker.nullness.qual.*;
public abstract class PureAndFlow {
@Nullable String s1;
@Nullable String s2;
void nonpure(String s1) {}
@org.checkerframework.dataflow.qual.Pure
// :: warning: (purity.deterministic.void.method)
void pure(String s2) {}
@org.checkerframework.dataflow.qual.Deterministic
// :: warning: (purity.deterministic.void.method)
void det(String s3) {}
@org.checkerframework.dataflow.qual.Pure
// :: warning: (purity.deterministic.void.method)
abstract void abstractpure(String s4);
@org.checkerframework.dataflow.qual.Deterministic
// :: warning: (purity.deterministic.void.method)
abstract void abstractdet(String s4);
void withNonRow() {
if (s2 != null) {
nonpure("m");
// :: error: (argument.type.incompatible)
pure(s2);
}
}
void withPure() {
if (s2 != null) {
pure("m");
pure(s2);
}
}
interface IFace {
@org.checkerframework.dataflow.qual.Pure
// :: warning: (purity.deterministic.void.method)
void ifacepure(String s);
@org.checkerframework.dataflow.qual.Deterministic
// :: warning: (purity.deterministic.void.method)
void ifacedet(String s);
}
class Cons {
@org.checkerframework.dataflow.qual.Pure
// :: warning: (purity.deterministic.constructor)
// :: error: (purity.not.deterministic.not.sideeffectfree.call.method)
Cons(String s) {}
@org.checkerframework.dataflow.qual.Deterministic
// :: warning: (purity.deterministic.constructor)
// :: error: (purity.not.deterministic.call.method)
Cons(int i) {}
}
}
|
