| import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| import org.checkerframework.dataflow.qual.Pure; |
| |
| public class ReadyReadLine { |
| |
| void m(MyBufferedReader buf) throws Exception { |
| if (buf.ready()) { |
| String line = buf.readLine(); |
| line.toString(); |
| } |
| |
| if (buf.readLine() != null) { |
| // :: error: (dereference.of.nullable) |
| buf.readLine().toString(); |
| } |
| } |
| } |
| |
| // This is a replication of the JDK BufferedReader, with only the relevant methods. |
| class MyBufferedReader { |
| public @Nullable String readLine() throws Exception { |
| return null; |
| } |
| |
| @EnsuresNonNullIf(expression = "readLine()", result = true) |
| @Pure |
| public boolean ready() throws Exception { |
| // don't bother with implementation. |
| // :: error: (contracts.conditional.postcondition) |
| return true; |
| } |
| } |