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
|
// Test case for issue #951:
// https://github.com/typetools/checker-framework/issues/951
import org.checkerframework.dataflow.qual.Deterministic;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.dataflow.qual.SideEffectFree;
public class Issue951 {
@Pure
public static int min(int[] a) {
if (a.length == 0) {
throw new MyExceptionSefConstructor("Empty array passed to min(int[])");
}
int result = a[0];
for (int i = 1; i < a.length; i++) {
result = min(result, a[i]);
}
return result;
}
@Pure
public static int arbitraryExceptionArg1() {
// :: error: (purity.not.deterministic.not.sideeffectfree.call.method)
// :: error: (purity.not.sideeffectfree.call.constructor)
throw new MyException("" + arbitraryMethod());
}
@Pure
public static int arbitraryExceptionArg2() {
// :: error: (purity.not.deterministic.not.sideeffectfree.call.method)
throw new MyExceptionSefConstructor("" + arbitraryMethod());
}
@Pure
public static int sefExceptionArg1() {
// The method is safe, so this is a false positive warning;
// in the future the Purity Checker may not issue this warning.
// :: error: (purity.not.deterministic.call.method)
// :: error: (purity.not.sideeffectfree.call.constructor)
throw new MyException("" + sefMethod());
}
@Pure
public static int sefExceptionArg2() {
// The method is safe, so this is a false positive warning;
// in the future the Purity Checker may not issue this warning.
// :: error: (purity.not.deterministic.call.method)
throw new MyExceptionSefConstructor("" + sefMethod());
}
@Pure
public static int detExceptionArg1() {
// :: error: (purity.not.sideeffectfree.call.method)
// :: error: (purity.not.sideeffectfree.call.constructor)
throw new MyException("" + detMethod());
}
@Pure
public static int detExceptionArg2() {
// :: error: (purity.not.sideeffectfree.call.method)
throw new MyExceptionSefConstructor("" + detMethod());
}
@Pure
public static int pureExceptionArg1(int a, int b) {
// :: error: (purity.not.sideeffectfree.call.constructor)
throw new MyException("" + min(a, b));
}
@Pure
public static int pureExceptionArg2(int a, int b) {
throw new MyExceptionSefConstructor("" + min(a, b));
}
@Pure
int throwNewWithinTry() {
for (int i = 0; i < 10; i++) {
try {
for (int j = 0; j < 10; j++) {
throw new MyExceptionSefConstructor("foo");
}
// :: error: (purity.not.deterministic.catch)
} catch (MyExceptionSefConstructor e) {
return -1;
}
}
return 22;
}
// Helper methods
// Not deterministic or side-effect-free
static int arbitraryMethod() {
return 22;
}
// Not deterministic
@SideEffectFree
static int sefMethod() {
return 22;
}
@Deterministic
// Not side-effect-free
static int detMethod() {
return 22;
}
@Pure
static int min(int a, int b) {
if (a < b) {
return a;
} else {
return b;
}
}
// Constructors
static class MyException extends Error {
// Not side-effect-free
MyException(String message) {}
}
static class MyExceptionSefConstructor extends Error {
// Side-effect-free
@SuppressWarnings("purity.not.sideeffectfree.call") // until java.util.Error is annotated
@SideEffectFree
MyExceptionSefConstructor(String message) {}
}
}
|
