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
|
import java.io.*;
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
public class FlowNonThis {
@Nullable String c;
public static void main(String[] args) {
FlowNonThis t = new FlowNonThis();
t.setup();
System.out.println(t.c.length());
t.erase();
// :: error: (dereference.of.nullable)
System.out.println(t.c.length());
}
public void setupThenErase() {
setup();
System.out.println(c.length());
erase();
// :: error: (dereference.of.nullable)
System.out.println(c.length());
}
public void justErase() {
// :: error: (dereference.of.nullable)
System.out.println(c.length());
erase();
// :: error: (dereference.of.nullable)
System.out.println(c.length());
}
@EnsuresNonNull("c")
public void setup() {
c = "setup";
}
public void erase() {
c = null;
}
}
|