| import org.checkerframework.checker.nullness.qual.*; |
| import org.checkerframework.dataflow.qual.*; |
| |
| public class PureTest { |
| @org.checkerframework.dataflow.qual.Pure |
| @Nullable Object puremethod(@Nullable Object a) { |
| return a; |
| } |
| |
| public void test() { |
| // :: error: (assignment) |
| @NonNull Object l0 = puremethod(null); |
| |
| if (puremethod(null) == null) { |
| // :: error: (assignment) |
| @NonNull Object l1 = puremethod(null); |
| } |
| |
| if (puremethod("m") != null) { |
| @NonNull Object l1 = puremethod("m"); |
| } |
| |
| if (puremethod("m") != null) { |
| // :: error: (assignment) |
| @NonNull Object l1 = puremethod(null); |
| } |
| |
| if (puremethod("m") != null) { |
| // :: error: (assignment) |
| @NonNull Object l1 = puremethod("n"); |
| } |
| |
| Object x = new Object(); |
| |
| if (puremethod(x) == null) { |
| return; |
| } |
| |
| @NonNull Object l2 = puremethod(x); |
| |
| x = new Object(); |
| |
| // :: error: (assignment) |
| @NonNull Object l3 = puremethod(x); |
| |
| // :: error: (assignment) |
| @NonNull Object l4 = puremethod("n"); |
| } |
| |
| public @org.checkerframework.dataflow.qual.Pure @Nullable Object getSuperclass() { |
| return null; |
| } |
| |
| static void shortCircuitAnd(PureTest pt) { |
| if ((pt.getSuperclass() != null) && pt.getSuperclass().equals(Enum.class)) { |
| // empty body |
| } |
| } |
| |
| static void shortCircuitOr(PureTest pt) { |
| if ((pt.getSuperclass() == null) || pt.getSuperclass().equals(Enum.class)) { |
| // empty body |
| } |
| } |
| |
| static void testInstanceofNegative(PureTest pt) { |
| if (pt.getSuperclass() instanceof Object) { |
| return; |
| } |
| // :: error: (dereference.of.nullable) |
| pt.getSuperclass().toString(); |
| } |
| |
| static void testInstanceofPositive(PureTest pt) { |
| if (!(pt.getSuperclass() instanceof Object)) { |
| return; |
| } |
| pt.getSuperclass().toString(); |
| } |
| |
| static void testInstanceofPositive2(PureTest pt) { |
| if (!(pt.getSuperclass() instanceof Object)) { |
| } else { |
| pt.getSuperclass().toString(); |
| } |
| } |
| |
| static void testInstanceofNegative2(PureTest pt) { |
| if (pt.getSuperclass() instanceof Object) { |
| } else { |
| return; |
| } |
| pt.getSuperclass().toString(); |
| } |
| |
| static void testInstanceofString(PureTest pt) { |
| if (!(pt.getSuperclass() instanceof String)) { |
| return; |
| } |
| pt.getSuperclass().toString(); |
| } |
| |
| static void testContinue(PureTest pt) { |
| for (; ; ) { |
| if (pt.getSuperclass() == null) { |
| System.out.println("m"); |
| continue; |
| } |
| pt.getSuperclass().toString(); |
| } |
| } |
| |
| void setSuperclass(@Nullable Object no) { |
| // set the field returned by getSuperclass. |
| } |
| |
| static void testInstanceofPositive3(PureTest pt) { |
| if (!(pt.getSuperclass() instanceof Object)) { |
| return; |
| } else { |
| pt.setSuperclass(null); |
| } |
| // :: error: (dereference.of.nullable) |
| pt.getSuperclass().toString(); |
| } |
| |
| @Override |
| @SideEffectFree |
| public String toString() { |
| return "foo"; |
| } |
| } |