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 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
|
import org.checkerframework.dataflow.qual.*;
import org.checkerframework.framework.qual.EnsuresQualifier;
import testlib.util.*;
class MethodCallFlowExpr {
@Pure
String p1(int i) {
return "";
}
@Pure
String p1b(Long i) {
return "";
}
@Pure
String p1(String s) {
return "";
}
String nonpure() {
return "";
}
@Pure
String p2(String s, long l, String s2) {
return "";
}
@Pure
<T> String p1c(T i) {
return "";
}
@Pure
static String p1d(int i) {
return "";
}
@EnsuresQualifier(expression = "p1c(\"abc\")", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e0() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "p1(1)", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e1() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "p1(\"abc\")", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e2() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "p2(\"abc\", 2L, p1(1))", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e4() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "p1b(2L)", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e5() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "p1b(null)", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e6() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "p1d(1)", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e7a() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "this.p1d(1)", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e7b() {
// don't bother with implementation
}
@EnsuresQualifier(expression = "MethodCallFlowExpr.p1d(1)", qualifier = Odd.class)
// :: error: (contracts.postcondition.not.satisfied)
void e7c() {
// don't bother with implementation
}
void t1() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1(1);
e1();
// :: error: (assignment.type.incompatible)
@Odd String l2 = p1(2);
@Odd String l3 = p1(1);
}
void t2() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1("abc");
e2();
// :: error: (assignment.type.incompatible)
@Odd String l2 = p1("def");
// :: error: (assignment.type.incompatible)
@Odd String l2b = p1(1);
@Odd String l3 = p1("abc");
}
void t3() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p2("abc", 2L, p1(1));
e4();
// :: error: (assignment.type.incompatible)
@Odd String l2 = p2("abc", 2L, p1(2));
// :: error: (assignment.type.incompatible)
@Odd String l2b = p2("abc", 1L, p1(1));
@Odd String l3 = p2("abc", 2L, p1(1));
}
void t4() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1b(2L);
e5();
// :: error: (assignment.type.incompatible)
@Odd String l2 = p1b(null);
// :: error: (assignment.type.incompatible)
@Odd String l2b = p1b(1L);
// FIXME: the following line shouldn't give an error
// (or at least it didn't give an error earlier)
// @Odd String l3 = p1b(2L);
}
void t5() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1b(null);
e6();
// :: error: (assignment.type.incompatible)
@Odd String l2 = p1b(1L);
// FIXME: the following line shouldn't give an error
// (or at least it didn't give an error earlier)
// @Odd String l3 = p1b(null);
}
void t6() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1c("abc");
e0();
// :: error: (assignment.type.incompatible)
@Odd String l2 = p1c("def");
@Odd String l3 = p1c("abc");
}
void t7() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1d(1);
// :: error: (assignment.type.incompatible)
@Odd String l1b = MethodCallFlowExpr.p1d(1);
// :: error: (assignment.type.incompatible)
@Odd String l1c = this.p1d(1);
e7a();
@Odd String l2 = p1d(1);
@Odd String l2b = MethodCallFlowExpr.p1d(1);
@Odd String l2c = this.p1d(1);
}
void t8() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1d(1);
// :: error: (assignment.type.incompatible)
@Odd String l1b = MethodCallFlowExpr.p1d(1);
// :: error: (assignment.type.incompatible)
@Odd String l1c = this.p1d(1);
e7b();
@Odd String l2 = p1d(1);
@Odd String l2b = MethodCallFlowExpr.p1d(1);
@Odd String l2c = this.p1d(1);
}
void t9() {
// :: error: (assignment.type.incompatible)
@Odd String l1 = p1d(1);
// :: error: (assignment.type.incompatible)
@Odd String l1b = MethodCallFlowExpr.p1d(1);
// :: error: (assignment.type.incompatible)
@Odd String l1c = this.p1d(1);
e7c();
@Odd String l2 = p1d(1);
@Odd String l2b = MethodCallFlowExpr.p1d(1);
@Odd String l2c = this.p1d(1);
}
}
|