| import org.checkerframework.checker.nullness.qual.*; |
| import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; |
| |
| public class ConditionalNullness { |
| |
| @EnsuresNonNullIf( |
| expression = {"field", "method()"}, |
| result = true) |
| boolean checkNonNull() { |
| // don't bother with the implementation |
| // :: error: (contracts.conditional.postcondition) |
| return true; |
| } |
| |
| @Nullable Object field = null; |
| |
| @org.checkerframework.dataflow.qual.Pure |
| @Nullable Object method() { |
| return "m"; |
| } |
| |
| void testSelfWithCheck() { |
| ConditionalNullness other = new ConditionalNullness(); |
| if (checkNonNull()) { |
| field.toString(); |
| method().toString(); |
| // :: error: (dereference.of.nullable) |
| other.field.toString(); // error |
| // :: error: (dereference.of.nullable) |
| other.method().toString(); // error |
| } |
| // :: error: (dereference.of.nullable) |
| method().toString(); // error |
| } |
| |
| void testSelfWithoutCheck() { |
| // :: error: (dereference.of.nullable) |
| field.toString(); // error |
| // :: error: (dereference.of.nullable) |
| method().toString(); // error |
| } |
| |
| void testSelfWithCheckNegation() { |
| if (checkNonNull()) { |
| // nothing to do |
| } else { |
| // :: error: (dereference.of.nullable) |
| field.toString(); // error |
| } |
| field.toString(); // error |
| } |
| |
| void testOtherWithCheck() { |
| ConditionalNullness other = new ConditionalNullness(); |
| if (other.checkNonNull()) { |
| other.field.toString(); |
| other.method().toString(); |
| // :: error: (dereference.of.nullable) |
| field.toString(); // error |
| // :: error: (dereference.of.nullable) |
| method().toString(); // error |
| } |
| // :: error: (dereference.of.nullable) |
| other.method().toString(); // error |
| // :: error: (dereference.of.nullable) |
| method().toString(); // error |
| } |
| |
| void testOtherWithoutCheck() { |
| ConditionalNullness other = new ConditionalNullness(); |
| // :: error: (dereference.of.nullable) |
| other.field.toString(); // error |
| // :: error: (dereference.of.nullable) |
| other.method().toString(); // error |
| // :: error: (dereference.of.nullable) |
| field.toString(); // error |
| // :: error: (dereference.of.nullable) |
| method().toString(); // error |
| } |
| |
| void testOtherWithCheckNegation() { |
| ConditionalNullness other = new ConditionalNullness(); |
| if (other.checkNonNull()) { |
| // nothing to do |
| } else { |
| // :: error: (dereference.of.nullable) |
| other.field.toString(); // error |
| // :: error: (dereference.of.nullable) |
| other.method().toString(); // error |
| // :: error: (dereference.of.nullable) |
| field.toString(); // error |
| } |
| // :: error: (dereference.of.nullable) |
| field.toString(); // error |
| } |
| } |