Merge ../checker-framework-branch-master into rlc-ioutils-stub

checker/build.gradle

@@ -481,11 +481,6 @@ task ainferTestCheckerGenerateAjava(type: Test) {
         // WPI; see the copy in the non-annotated WPI tests for an explanation.
         delete('tests/ainfer-testchecker/annotated/all-systems/java8/memberref/Purity.java')
 
-        // These tests cause an error like the following when their corresponding ajava files are read:
-        // :0: warning: Annotations-org.checkerframework.common.value.ValueChecker.ajava:(line 3,col 1): Skipping annotation type: Anno
-        delete('tests/ainfer-testchecker/annotated/all-systems/Annotations.java')
-        delete('tests/ainfer-testchecker/annotated/all-systems/Issue4083.java')
-
         // There is some kind of bad interaction between the purity checker's inference mode
         // and method references to constructors: every one of them in this test causes a
         // purity.methodref warning during validation. This problem only occurs for ajava-based

checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub

@@ -0,0 +1,40 @@
+// This stub file makes the Nullness Checker not warn about null pointer
+// exceptions thrown by nullness assertion methods.  There is no longer any
+// guarantee that your program will not throw a NullPointerException.
+
+import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import java.util.function.Supplier;
+
+
+package java.util;
+
+public class Objects {
+    @EnsuresNonNull("#1")
+    public static <T> T requireNonNull(@Nullable T obj);
+    @EnsuresNonNull("#1")
+    public static <T> T requireNonNull(@Nullable T obj, String message);
+}
+
+
+// No annotations for com.google.common.base.Preconditions or
+// com.google.common.base.Verify are needed because they are annotated with
+// @CheckForNull and the Checker Framework treats @CheckForNull as @Nullable.
+
+
+package org.junit;
+
+public class Assertions {
+  public static void assertNotNull(@Nullable Object actual);
+  public static void assertNotNull(@Nullable Object actual, String message);
+  public static void assertNotNull(@Nullable Object actual, Supplier<String> messageSupplier);
+}
+
+
+package org.junit.jupiter.api;
+
+public class Assertions {
+  public static void assertNotNull(@Nullable Object actual);
+  public static void assertNotNull(@Nullable Object actual, String message);
+  public static void assertNotNull(@Nullable Object actual, Supplier<String> messageSupplier);
+}

docs/CHANGELOG.md

@@ -6,6 +6,9 @@ Version 3.28.1 (January 3, 2022)
 Dropped support for `-ApermitUnsupportedJdkVersion` command-line argument.
 You can now run the Checker Framework under any JDK version, without a warning.
 
+Pass `-Astubs=permit-nullness-assertion-exception.astub` to not be warned about null
+pointer exceptions within nullness assertion methods like `Objects.requireNonNull`.
+
 Pass `-Astubs=sometimes-nullable.astub` to unsoundly permit passing null to
 calls if null is sometimes but not always permitted.
 

docs/manual/introduction.tex

@@ -1262,6 +1262,7 @@
   java.lang.Objects.requireNonNull(Object)
   java.lang.String.contains(CharSequence)
   org.junit.Assert.assertNotNull(Object)
+  org.junit.jupiter.api.Assert.assertNotNull(Object)
 \end{Verbatim}
 
 Their formal parameter type is annotated as \<@NonNull>, because otherwise the
@@ -1313,6 +1314,11 @@
 \item
   A stub file (Section~\ref{stub}) can override the library's annotations,
   for one or more methods.
+
+  As a special case, if you want the Nullness Checker to prevent most null
+  pointer exceptions in your code, but to \emph{permit} null pointer
+  exceptions at nullness assertion methods, you can pass
+  \<-Astubs=permit-nullness-assertion-exception.astub>.
 \item
   Don't type-check clients of the method.  For example, JUnit's
   \<assertNotNull()> is typically called only in test code; its clients are

docs/manual/warnings.tex

@@ -447,7 +447,7 @@
 has independently verified to be true.  The Checker Framework can
 leverage these assertions in order to avoid issuing false positive
 warnings.  The programmer marks such assertions with the \<@AssumeAssertion>
-string in the \<assert> message (see Section~\ref{assumeassertion}.  Only
+string in the \<assert> message (see Section~\ref{assumeassertion}).  Only
 do so if you are sure that the assertion always succeeds at run time.
 
 \label{assertion-methods}
@@ -471,13 +471,23 @@
 \refmethod{checker/nullness/util}{NullnessUtil}{castNonNull}{-T-} is not an
 assertion method.  It is a warning suppression method.
 
-Note that some libraries have an imprecise specification of their assertion
-methods.  For example, Guava's \<Verify.verifyNotNull> is imprecisely
+Note that some libraries have an imprecise/incorrect specification of their assertion
+methods.  For example, Guava's \<Verify.verifyNotNull> is imprecisely/incorrectly
 specified to have a \<@Nullable> formal parameter.  In a correct execution,
 \<null> never flows there, so its type can and should be annotated as
 \<@NonNull>.  That annotation allows the Nullness Checker to warn about
-programs that crash due to passing \<null> to \<verifyNotNull>.  You can
-use a version of Guava with a small change to your build file.  Where the
+programs that crash due to passing \<null> to \<verifyNotNull>.
+(A comment in Guava's \<Preconditions.java> agrees with this reasoning:
+``the first parameter to \<checkNotNull> \emph{should} be annotated to
+require it to be non-null.''  The comment goes on to say ``I had hoped to
+take a principled stand on this'' (that, is, write the annotation
+\<@NonNull>), but Guava annotates it as \<@Nullable> to accommodate misuses
+within the Google codebase.)
+
+By default, the Checker Framework uses Guava's annotations as written.  If
+you wish to  take the principled stand in order to prevent \emph{all}
+\<NullPointerException>s, you can
+use a different version of Guava with a small change to your build file.  Where the
 build file refers to Maven Central's \<guava> artifact, change the group
 name from ``com.google.guava'' to ``org.checkerframework.annotatedlib''.
 (The code is identical; the only difference is annotations.)
@@ -519,6 +529,11 @@
   If the method is defined in an external library, write a stub file that
   changes the method's annotations, or use \<-AskipUses> to make the
   Checker Framework ignore all calls to an entire class.
+
+  As a special case, if you want the Nullness Checker to prevent most null
+  pointer exceptions in your code, but to \emph{permit} null pointer
+  exceptions at nullness assertion methods, you can pass
+  \<-Astubs=permit-nullness-assertion-exception.astub>.
 \end{itemize}
 
 
@@ -715,6 +730,12 @@
 }
 \end{Verbatim}
 
+This particular stub file already exists.
+If you want the Nullness Checker to prevent most null
+pointer exceptions in your code, but to \emph{permit} null pointer
+exceptions at nullness assertion methods, you can pass
+\<-Astubs=permit-nullness-assertion-exception.astub>.
+
 
 \sectionAndLabel{Don't run the processor}{no-processor}
 
@@ -746,17 +767,17 @@
 % LocalWords:  checkername util myref nulltest html ESC buildfile mynifty Fenum
 % LocalWords:  MyNiftyChecker messagekey basetype uncommenting Anomsgtext
 % LocalWords:  AskipDefs mypackage Makefile PLXCOMP expr
-%  LocalWords:  TODO AsuppressWarnings AssumeAssertion AonlyUses AonlyDefs
-%  LocalWords:  ing warningkey redundantNullComparison qual proc Decl
-%  LocalWords:  lastsinglesuppression classfiles AwarnUnneededSuppressions
-%%  LocalWords:  AshowSuppressWarningsStrings NullableType NonNullType JUnit's
-%%  LocalWords:  PolyNullType MonotonicNonNullType KeyForType NullableDecl
-%%  LocalWords:  NonNullDecl PolyNullDecl MonotonicNonNullDecl KeyForDecl
-%%  LocalWords:  refactored AassumeAssertionsAreEnabled assertNotNull
-%%  LocalWords:  AassumeAssertionsAreDisabled NullnessUtil checkNotNull
-%%  LocalWords:  ElementType AuseSafeDefaultsForUnannotatedSourceCode
+% LocalWords:  TODO AsuppressWarnings AssumeAssertion AonlyUses AonlyDefs
+% LocalWords:  ing warningkey redundantNullComparison qual proc Decl
+% LocalWords:  lastsinglesuppression classfiles AwarnUnneededSuppressions
+% LocalWords:  AshowSuppressWarningsStrings NullableType NonNullType JUnit's
+% LocalWords:  PolyNullType MonotonicNonNullType KeyForType NullableDecl
+% LocalWords:  NonNullDecl PolyNullDecl MonotonicNonNullDecl KeyForDecl
+% LocalWords:  refactored AassumeAssertionsAreEnabled assertNotNull
+% LocalWords:  AassumeAssertionsAreDisabled NullnessUtil checkNotNull
+% LocalWords:  ElementType AuseSafeDefaultsForUnannotatedSourceCode
 % LocalWords:  AuseConservativeDefaultsForUncheckedCode checkerframework askipuses
-%%  LocalWords:  suppresswarnings ArequirePrefixInWarningSuppressions
-%%  LocalWords:  assumeassertion askipdefs alint compat substring myGet
+% LocalWords:  suppresswarnings ArequirePrefixInWarningSuppressions
+% LocalWords:  assumeassertion askipdefs alint compat substring myGet
 % LocalWords:  AcheckPurityAnnotations allcheckers requireNonNull
 % LocalWords:  verifyNotNull subcheckers subchecker

framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java

@@ -932,8 +932,10 @@ private List<AnnotatedTypeVariable> processTypeDecl(
                 + "...");
         return null;
       }
-      stubWarnNotFound(typeDecl, "Skipping annotation type: " + fqTypeName);
+      typeDeclTypeParameters = processType(typeDecl, typeElt);
+      typeParameters.addAll(typeDeclTypeParameters);
     } else if (typeDecl instanceof ClassOrInterfaceDeclaration) {
+      // TODO: This test is never satisfied, because it is the opposite of that on the line above.
       if (!(typeDecl instanceof ClassOrInterfaceDeclaration)) {
         warn(
             typeDecl,