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
|
import org.checkerframework.dataflow.qual.Pure;
import org.checkerframework.framework.test.*;
import testlib.util.*;
/** Various tests for annotation aliasing. */
class AnnotationAliasing {
String f1, f2, f3;
@Pure
int pure1() {
return 1;
};
@org.jmlspecs.annotation.Pure
int pure2() {
return 1;
};
// a method that is not pure (no annotation)
void nonpure() {}
@Pure
String t1() {
// :: error: (purity.not.deterministic.not.sideeffectfree.call.method)
nonpure();
return "";
}
@org.jmlspecs.annotation.Pure
String t2() {
// :: error: (purity.not.deterministic.not.sideeffectfree.call.method)
nonpure();
return "";
}
// check aliasing of Pure
void t1(@Odd String p1, String p2) {
f1 = p1;
@Odd String l2 = f1;
pure1();
@Odd String l3 = f1;
pure2();
@Odd String l4 = f1;
}
}
|
