Report irrelevant @NonNull annotations (#153)

src/main/java/com/google/jspecify/nullness/NullSpecVisitor.java

@@ -28,6 +28,7 @@
 import static javax.lang.model.element.ElementKind.ENUM_CONSTANT;
 import static javax.lang.model.element.ElementKind.PACKAGE;
 import static org.checkerframework.framework.util.AnnotatedTypes.asSuper;
+import static org.checkerframework.javacutil.AnnotationUtils.annotationName;
 import static org.checkerframework.javacutil.AnnotationUtils.areSameByName;
 import static org.checkerframework.javacutil.TreeUtils.annotationsFromTypeAnnotationTrees;
 import static org.checkerframework.javacutil.TreeUtils.elementFromDeclaration;
@@ -579,15 +580,21 @@ private void checkNoNullnessAnnotations(
        * represent the types internally in AnnotatedTypeMirror instances. Contrast this to almost
        * all other logic in the checker, which operates on the internal types.
        */
-      if (areSameByName(annotation, "org.jspecify.annotations.Nullable")
-          || areSameByName(annotation, "org.jspecify.annotations.NullnessUnspecified")
-          || areSameByName(annotation, "org.jspecify.nullness.Nullable")
-          || areSameByName(annotation, "org.jspecify.nullness.NullnessUnspecified")) {
-        checker.reportError(treeToReportOn, messageKey);
+      if (NULLNESS_ANNOTATIONS.stream().anyMatch(na -> areSameByName(annotation, na))) {
+        checker.reportError(treeToReportOn, messageKey, annotationName(annotation));
       }
     }
   }
 
+  private static final Set<String> NULLNESS_ANNOTATIONS =
+      Set.of(
+          "org.jspecify.annotations.NonNull",
+          "org.jspecify.annotations.Nullable",
+          "org.jspecify.annotations.NullnessUnspecified",
+          "org.jspecify.nullness.NonNull",
+          "org.jspecify.nullness.Nullable",
+          "org.jspecify.nullness.NullnessUnspecified");
+
   @Override
   protected boolean checkMethodReferenceAsOverride(MemberReferenceTree tree, Void p) {
     /*

src/main/resources/com/google/jspecify/nullness/messages.properties

@@ -1,9 +1,9 @@
 atomicreference.must.include.null=expected a @Nullable type argument or else an initial-value constructor argument. The no-arg AtomicReference constructor sets the initial value to null, which is not compatible with %s.
 dereference=possible null dereference on type %s
 enum.constant.annotated=illegal location for annotation: enum constants are always non-null
-local.variable.annotated=illegal location for annotation: local variables have their nullness automatically inferred (except for their type arguments, as in `List<@Nullable String>`)
+local.variable.annotated=illegal location for annotation %s: local variables have their nullness automatically inferred (except for their type arguments, as in `List<@Nullable String>`)
 outer.annotated=illegal location for annotation: outer types are always non-null. To annotate the inner type, write `Foo.@Nullable Bar` instead of `@Nullable Foo.Bar`.
-primitive.annotated=illegal location for annotation: primitives are always non-null. To annotate an array of primitives as nullable, write `int @Nullable[]` instead of `@Nullable int[]`.
+primitive.annotated=illegal location for annotation %s: primitives are always non-null. To annotate an array of primitives as nullable, write `int @Nullable[]` instead of `@Nullable int[]`.
 threadlocal.must.include.null=expected a @Nullable type argument or else an override of initialValue(). Without an override of initialValue(), ThreadLocal.get() may return null, which is not compatible with %s.
-type.parameter.annotated=illegal location for annotation: type parameter declarations do not have a nullness. To declare that a type parameter may be instantiated with nullable types, write `T extends @Nullable Object` instead of `@Nullable T`.
-wildcard.annotated=illegal location for annotation: wildcard declarations do not have a nullness. To declare that a wildcard may match nullable types, write `? extends @Nullable Object` instead of `@Nullable ?`. Or, in null-aware code, simply write `?`.
+type.parameter.annotated=illegal location for annotation %s: type parameter declarations do not have a nullness. To declare that a type parameter may be instantiated with nullable types, write `T extends @Nullable Object` instead of `@Nullable T`.
+wildcard.annotated=illegal location for annotation %s: wildcard declarations do not have a nullness. To declare that a wildcard may match nullable types, write `? extends @Nullable Object` instead of `@Nullable ?`. Or, in null-aware code, simply write `?`.

src/test/java/tests/ConformanceTest.java

@@ -209,7 +209,13 @@ protected String getFactText() {
         return cannotConvert(sourceType, sinkType);
       }
       if (IRRELEVANT_ANNOTATION_KEYS.contains(detailMessage.messageKey)) {
-        return irrelevantAnnotation("Nullable"); // TODO(dpb): Support other annotations.
+        if (detailMessage.messageArguments.isEmpty()) {
+          // arguments must start with the annotation
+          return toString();
+        }
+        return irrelevantAnnotation(
+            // Remove the package name (and any enclosing element name); emit just the simple name.
+            detailMessage.messageArguments.get(0).replaceFirst(".*\\.", ""));
       }
       switch (detailMessage.messageKey) {
         case "sourceType":