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
|
// Test case for Issue 1406
// https://github.com/typetools/checker-framework/issues/1406
import java.util.ArrayList;
import java.util.List;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.dataflow.qual.Pure;
@SuppressWarnings({"purity", "contracts.postcondition.not.satisfied"}) // Only test parsing
public class Issue1406 {
public static void main(String[] args) {}
@Pure
@EnsuresNonNull("myMethod(#1).get(0)")
List<String> myMethod(int arg) {
List<String> result = new ArrayList<>();
result.add("non-null value");
return result;
}
String client(int arg) {
return myMethod(arg).get(0);
}
@Pure
@EnsuresNonNull("myMethod2().get(0)")
List<String> myMethod2() {
List<String> result = new ArrayList<>();
result.add("non-null value");
return result;
}
String client2() {
return myMethod2().get(0);
}
}
|
