The resolver needs access to classes, in order to parse Java expressi…

…ons (#5970)

docs/manual/advanced-features.tex

@@ -1358,11 +1358,21 @@
 %% TODO: we may eventually have an @SpecField annotation
 
 
-\textbf{Limitations:}
+\subsectionAndLabel{Limitations}{java-expressions-limitations}
+
+If you mention a class in a Java expression, then that class must be
+available to the compiler.  For example, if you write
+  \<@EnsuresNonNull("package1.package2.MyClass.myField.myOtherField")>,
+then you should pass \<MyClass.java> to the compiler.  Otherwise, the
+compiler does not know which components of the dotted name are packages,
+classes, and field names.  In that case, you might get confusing error
+messages such as ``Invalid 'package1.package2' because could not find class
+package1 in package package2''.
+
 It is not possible to write a
 quantification over all array components (e.g., to express that all
-  array elements are non-null).  There is no such Java expression, but it
-  would be useful when writing specifications.
+array elements are non-null).  There is no such Java expression, but it
+would be useful when writing specifications.
 
 
 \sectionAndLabel{Field invariants}{field-invariants}

framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java

@@ -624,7 +624,8 @@ public JavaExpression visit(NameExpr expr, Void aVoid) {
         }
       }
 
-      // Construct a FieldAccess expression.
+      // `fieldElem` is now set.  Construct a FieldAccess expression.
+
       if (ElementUtils.isStatic(fieldElem)) {
         Element classElem = fieldElem.getEnclosingElement();
         JavaExpression staticClassReceiver = new ClassName(ElementUtils.getType(classElem));
@@ -782,8 +783,11 @@ private ExecutableElement getMethodElement(
       throw constructJavaExpressionParseError(methodName, "no such method");
     }
 
-    // expr is a field access, a fully qualified class name, or a class name qualified with
-    // another class name (e.g. {@code OuterClass.InnerClass})
+    // `expr` should be a field access, a fully qualified class name, or a class name qualified with
+    // another class name (e.g. {@code OuterClass.InnerClass}).
+    // If the expression refers to a class that is not available to the resolver (the class wasn't
+    // passed to javac on the command line), then the argument can be "outerpackage.innerpackage",
+    // which will lead to a confusing error message.
     @Override
     public JavaExpression visit(FieldAccessExpr expr, Void aVoid) {
       setResolverField();