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
|
import org.checkerframework.dataflow.qual.Deterministic;
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.framework.test.*;
import testlib.util.*;
// various tests about keeping information in the store about pure method calls
class StorePure {
String f1, f2;
// various pure methods
@Pure
String pure1() {
return null;
}
@Pure
String pure1b() {
return null;
}
@Deterministic
String pure1c() {
return null;
}
@Pure
String pure2(int i) {
return null;
}
@Pure
String pure3(boolean b) {
return null;
}
@Pure
String pure4(String o) {
return null;
}
void nonpure() {}
void t1(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure1() == p1) {
@Odd String l1 = pure1();
l0 = "a"; // does not remove information
@Odd String l1b = pure1();
// :: error: (assignment.type.incompatible)
@Odd String l2 = pure1b();
nonpure(); // non-pure method call might change the return value of pure1
// :: error: (assignment.type.incompatible)
@Odd String l3 = pure1();
}
}
// check that it only works for deterministic methods
void t1b(@Odd String p1, String p2, boolean b1) {
if (pure1c() == p1) {
@Odd String l1 = pure1c();
}
}
void t2(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure1() == p1) {
@Odd String l1 = pure1();
l0 = "a"; // does not remove information
@Odd String l1b = pure1();
// :: error: (assignment.type.incompatible)
@Odd String l2 = pure1b();
f1 = ""; // field update might change the return value of pure1
// :: error: (assignment.type.incompatible)
@Odd String l3 = pure1();
}
}
void t3(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure2(1) == p1) {
// :: error: (assignment.type.incompatible)
@Odd String l4 = pure2(0);
@Odd String l1 = pure2(1);
l0 = "a"; // does not remove information
@Odd String l1b = pure2(1);
nonpure(); // non-pure method call might change the return value of pure2
// :: error: (assignment.type.incompatible)
@Odd String l3 = pure2(1);
}
}
void t4(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure2(1) == p1) {
// :: error: (assignment.type.incompatible)
@Odd String l4 = pure2(0);
@Odd String l1 = pure2(1);
l0 = "a"; // does not remove information
@Odd String l1b = pure2(1);
f1 = ""; // field update might change the return value of pure2
// :: error: (assignment.type.incompatible)
@Odd String l3 = pure2(1);
}
}
void t5(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure3(true) == p1) {
// :: error: (assignment.type.incompatible)
@Odd String l4 = pure3(false);
@Odd String l1 = pure3(true);
l0 = "a"; // does not remove information
@Odd String l1b = pure3(true);
nonpure(); // non-pure method call might change the return value of pure2
// :: error: (assignment.type.incompatible)
@Odd String l3 = pure3(true);
}
}
void t6(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure3(true) == p1) {
// :: error: (assignment.type.incompatible)
@Odd String l4 = pure3(false);
@Odd String l1 = pure3(true);
l0 = "a"; // does not remove information
@Odd String l1b = pure3(true);
f1 = ""; // field update might change the return value of pure2
// :: error: (assignment.type.incompatible)
@Odd String l3 = pure3(true);
}
}
// local variable as argument
void t7(@Odd String p1, String p2, boolean b1) {
String l0 = "";
if (pure4(l0) == p1) {
// :: error: (assignment.type.incompatible)
@Odd String l4 = pure4("jk");
@Odd String l1 = pure4(l0);
l0 = "a"; // remove information (!)
// :: error: (assignment.type.incompatible)
@Odd String l1b = pure4(l0);
}
}
}
|
