Class CheckerFrameworkWPIPerDirectoryTest

java.lang.Object
org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest
org.checkerframework.framework.test.CheckerFrameworkWPIPerDirectoryTest
Direct Known Subclasses:
AinferGeneratePerDirectoryTest, AinferValidatePerDirectoryTest

public abstract class CheckerFrameworkWPIPerDirectoryTest extends CheckerFrameworkPerDirectoryTest
A specialized variant of CheckerFrameworkPerDirectoryTest for testing the Whole Program Inference feature of the Checker Framework, which is tested by running pairs of these tests: a "generation test" (of class AinferGeneratePerDirectoryTest) to do inference using the -Ainfer option, and a "validation test" (of class AinferValidatePerDirectoryTest) to check that files typecheck after those inferences are taken into account. This common superclass of those two classes should never be used directly.
  • Constructor Details

  • Method Details

    • doNotTypecheck

      protected void doNotTypecheck(@UnderInitialization(CheckerFrameworkPerDirectoryTest.class) CheckerFrameworkWPIPerDirectoryTest this, String endswith)
      Do not typecheck any file ending with the given String. A subclass of CheckerFrameworkWPIPerDirectoryTest uses this routine to avoid typechecking files in the all-systems test suite that are problematic for one typechecker. For example, this routine is useful when running the all-systems tests using WPI, because some all-systems tests have expected errors that become warnings during a WPI run (because of -Awarns) and so must be excluded.

      This code takes advantage of the mutability of the CheckerFrameworkPerDirectoryTest.testFiles field.

      Parameters:
      endswith - a string that the absolute path of the target file that should not be typechecked ends with. Usually, this takes the form "all-systems/ProblematicFile.java".
    • hasSkipComment

      public static boolean hasSkipComment(File file, String skipComment)
      Whether file contains skipComment.
      Parameters:
      file - a java test file
      skipComment - a comment that indicates that a test should be skipped
      Returns:
      whether file contains skipComment
    • resolveTestDirectory

      protected File resolveTestDirectory()
      Resolves the test root directory from the optional TestRootDirectory annotation or falls back to the default of currentDir/tests.
      Returns:
      the resolved directory
    • checkResult

      public void checkResult(TypecheckResult typecheckResult)
      Check that the TypecheckResult did not fail.
      Parameters:
      typecheckResult - result to check