diff --git a/checker/jtreg/nullness/issue3700/Client.out b/checker/jtreg/nullness/issue3700/Client.out
index f0d8acb7579..248618f6aa9 100644
--- a/checker/jtreg/nullness/issue3700/Client.out
+++ b/checker/jtreg/nullness/issue3700/Client.out
@@ -1,2 +1,2 @@
-warning: TimeUnitRange.astub:(line 3,col 1): TimeUnitRange is an enum, but stub file declared it as class TimeUnitRange {...
+warning: TimeUnitRange.astub:(line 3,col 1): TimeUnitRange is an enum, but stub file declared it as class TimeUnitRange { public TimeUnitRange of(@Nullable String endUnit); }
1 warning
diff --git a/checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java b/checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java
new file mode 100644
index 00000000000..fcfbb134d7d
--- /dev/null
+++ b/checker/tests/ainfer-testchecker/non-annotated/OptionGroup.java
@@ -0,0 +1,18 @@
+// This annotation from plume-lib options caused an error in
+// a version of ajava-based WPI. The problem was that annotation
+// declarations weren't considered possible declarations when checking
+// whether a location can store a declaration annotation.
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.RUNTIME)
+@Target(ElementType.FIELD)
+public @interface OptionGroup {
+
+ String value();
+
+ boolean unpublicized() default false;
+}
diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/SceneToStubWriter.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/SceneToStubWriter.java
index 65619fafc51..5ce68c8c1cb 100644
--- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/SceneToStubWriter.java
+++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/SceneToStubWriter.java
@@ -546,8 +546,14 @@ private static int printClassDefinitions(
// file, which will eventually be merged with this one.
printWriter.print(formatAnnotations(aClass.getAnnotations()));
}
- if (aClass.isEnum(nameToPrint)) {
+ if (aClass.isAnnotation(nameToPrint)) {
+ printWriter.print("@interface ");
+ } else if (aClass.isEnum(nameToPrint)) {
printWriter.print("enum ");
+ } else if (aClass.isInterface(nameToPrint)) {
+ printWriter.print("interface ");
+ } else if (aClass.isRecord(nameToPrint)) {
+ printWriter.print("record ");
} else {
printWriter.print("class ");
}
diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/scenelib/ASceneWrapper.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/scenelib/ASceneWrapper.java
index f1eef8fcb71..1f9ced18b49 100644
--- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/scenelib/ASceneWrapper.java
+++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/scenelib/ASceneWrapper.java
@@ -217,8 +217,14 @@ public void updateSymbolInformation(AClass aClass, @Nullable ClassSymbol classSy
ClassSymbol outerClass = classSymbol;
ClassSymbol previous = classSymbol;
do {
- if (outerClass.isEnum()) {
+ if (outerClass.getKind() == ElementKind.ANNOTATION_TYPE) {
+ aClass.markAsAnnotation(outerClass.getSimpleName().toString());
+ } else if (outerClass.isEnum()) {
aClass.markAsEnum(outerClass.getSimpleName().toString());
+ } else if (outerClass.isInterface()) {
+ aClass.markAsInterface(outerClass.getSimpleName().toString());
+ // } else if (outerClass.isRecord()) {
+ // aClass.markAsRecord(outerClass.getSimpleName().toString());
}
Element element = classSymbol.getEnclosingElement();
if (element == null || element.getKind() == ElementKind.PACKAGE) {
diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java
index 462e917cd63..dc425875cd9 100644
--- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java
+++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java
@@ -849,6 +849,28 @@ private boolean skipNode(NodeWithAccessModifiers<?> node) {
&& node.getModifiers().contains(Modifier.privateModifier());
}
+ /**
+ * Returns the string representation of {@code n}, one one line, truncated to {@code length}
+ * characters.
+ *
+ * @param n a JavaParser node
+ * @param length the maximum length of the string representation
+ * @return the truncated string representation of {@code n}
+ */
+ private String javaParserNodeToStringTruncated(Node n, int length) {
+ String oneLine =
+ n.toString()
+ .replace("\t", " ")
+ .replace("\n", " ")
+ .replace("\r", " ")
+ .replaceAll(" +", " ");
+ if (oneLine.length() <= length) {
+ return oneLine;
+ } else {
+ return oneLine.substring(0, length - 3) + "...";
+ }
+ }
+
/**
* Process a type declaration: copy its annotations to {@code #annotationFileAnnos}.
*
@@ -916,8 +938,7 @@ private List<AnnotatedTypeVariable> processTypeDecl(
typeDecl,
innerName
+ " is an enum, but stub file declared it as "
- + typeDecl.toString().split("\\R", 2)[0]
- + "...");
+ + javaParserNodeToStringTruncated(typeDecl, 100));
return null;
}
typeDeclTypeParameters = processEnum((EnumDeclaration) typeDecl, typeElt);
@@ -928,8 +949,7 @@ private List<AnnotatedTypeVariable> processTypeDecl(
typeDecl,
innerName
+ " is an annotation, but stub file declared it as "
- + typeDecl.toString().split("\\R", 2)[0]
- + "...");
+ + javaParserNodeToStringTruncated(typeDecl, 100));
return null;
}
typeDeclTypeParameters = processType(typeDecl, typeElt);
@@ -941,8 +961,7 @@ private List<AnnotatedTypeVariable> processTypeDecl(
typeDecl,
innerName
+ " is a class or interface, but stub file declared it as "
- + typeDecl.toString().split("\\R", 2)[0]
- + "...");
+ + javaParserNodeToStringTruncated(typeDecl, 100));
return null;
}
typeDeclTypeParameters = processType(typeDecl, typeElt);
diff --git a/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java b/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java
index 13e1ada2a9a..4a7d7c47bf7 100644
--- a/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java
+++ b/framework/src/main/java/org/checkerframework/framework/stub/StubGenerator.java
@@ -191,11 +191,19 @@ private void printClass(TypeElement typeElement, @Nullable String outerClass) {
}
}
- if (typeElement.getKind() == ElementKind.INTERFACE) {
+ // This could be a `switch` statement.
+ if (typeElement.getKind() == ElementKind.ANNOTATION_TYPE) {
+ out.print("@interface");
+ } else if (typeElement.getKind() == ElementKind.ENUM) {
+ out.print("enum");
+ } else if (typeElement.getKind() == ElementKind.INTERFACE) {
out.print("interface");
+ } else if (typeElement.getKind().name().equals("RECORD")) {
+ out.print("record");
} else if (typeElement.getKind() == ElementKind.CLASS) {
out.print("class");
} else {
+ // Shouldn't this throw an exception?
return;
}
diff --git a/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java b/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java
index b10971e9504..f87e5a14972 100644
--- a/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java
+++ b/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java
@@ -8,6 +8,7 @@
import com.github.javaparser.ast.CompilationUnit;
import com.github.javaparser.ast.Node;
import com.github.javaparser.ast.StubUnit;
+import com.github.javaparser.ast.body.AnnotationDeclaration;
import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
import com.github.javaparser.ast.body.EnumDeclaration;
import com.github.javaparser.ast.body.TypeDeclaration;
@@ -221,6 +222,11 @@ public static TypeDeclaration<?> getTypeDeclarationByName(CompilationUnit root,
return enumDecl.get();
}
+ Optional<AnnotationDeclaration> annoDecl = root.getAnnotationDeclarationByName(name);
+ if (annoDecl.isPresent()) {
+ return annoDecl.get();
+ }
+
Optional<CompilationUnit.Storage> storage = root.getStorage();
if (storage.isPresent()) {
throw new BugInCF("Type " + name + " not found in " + storage.get().getPath());