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
|
import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.dataflow.qual.*;
public class EnsuresNonNullIfTest4 {
public void add_bottom_up(MyInvariant inv) {
// The problem goes away if the below line is deleted or replaced with:
// Object x = new Object[100];
Object x = new @Nullable Object[100];
if (inv.is_ni_suppressed()) {
Object ss = inv.get_ni_suppressions();
ss.toString();
}
}
}
class MyInvariant {
@Pure
public @Nullable Object get_ni_suppressions() {
return (null);
}
@SuppressWarnings("nullness")
@EnsuresNonNullIf(result = true, expression = "get_ni_suppressions()")
@Pure
public boolean is_ni_suppressed() {
return true;
}
}
|