diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index f99a704881c..591465bdbfb 100644 --- a/docs/manual/advanced-features.tex +++ b/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 \ 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} diff --git a/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java b/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java index dd9dbf983fe..b127852590d 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java +++ b/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();