checker/tests/nullness/EnsuresNonNullIfTest.java

// Test case for issue 62: https://github.com/typetools/checker-framework/issues/62

// @skip-test until the issue is fixed

import org.checkerframework.checker.nullness.qual.*;
import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf;

public class EnsuresNonNullIfTest {

  public static void fromDirPos(File1 dbdir) {
    if (dbdir.isDirectory()) {
      File1 @NonNull [] files = dbdir.listFiles();
    }
  }

  public static void fromDirNeg(File1 dbdir) {
    if (!dbdir.isDirectory()) {
      throw new Error("Not a directory: " + dbdir);
    }
    File1 @NonNull [] files = dbdir.listFiles();
  }
}

///////////////////////////////////////////////////////////////////////////
/// Classes copied from the annotated JDK
///

// NOTE:  These annotations are actually incorrect (& not in the JDK).
// But, the test remains valid in how it exercises nullness checking.

// TODO: Have a way of saying the property holds no matter what value is used in a given expression.

public class File1 {
  @EnsuresNonNullIf(
      result = true,
      expression = {
        "list()",
        "list(String)", // TODO: has no effect
        "listFiles()",
        "listFiles(String)", // TODO: has no effect
        "listFiles(Double)" // TODO: has no effect
      })
  public boolean isDirectory() {
    throw new RuntimeException("skeleton method");
  }

  public String @Nullable [] list() {
    throw new RuntimeException("skeleton method");
  }

  public String @Nullable [] list(@Nullable String FilenameFilter_a1) {
    throw new RuntimeException("skeleton method");
  }

  public File1 @Nullable [] listFiles() {
    throw new RuntimeException("skeleton method");
  }

  public File1 @Nullable [] listFiles(@Nullable String FilenameFilter_a1) {
    throw new RuntimeException("skeleton method");
  }

  public File1 @Nullable [] listFiles(@Nullable Double FileFilter_a1) {
    throw new RuntimeException("skeleton method");
  }
}