Improve the documentation of Receiver (#3473)

dataflow/src/main/java/org/checkerframework/dataflow/analysis/FlowExpressions.java

@@ -446,9 +446,23 @@ private static Receiver internalReprOfMemberSelect(
         return internalArguments;
     }
 
+    // The syntax that the Checker Framework uses for Java expressions also includes "<self>" and
+    // "#1" for formal parameters.  However, there are no special subclasses (AST nodes) for those
+    // extensions.
     /**
-     * The poorly-named Receiver class is actually a Java AST. Each subclass represents a different
-     * type of expression, such as MethodCall, ArrayAccess, LocalVariable, etc.
+     * This class represents a Java expression and its type. It does not represent all possible Java
+     * expressions (for example, it does not represent a ternary expression; use {@link
+     * FlowExpressions.Unknown} for unrepresentable expressions).
+     *
+     * <p>This class's representation is like an AST: subparts are also expressions. For declared
+     * names (fields, local variables, and methods), it also contains an Element.
+     *
+     * <p>Each subclass represents a different type of expression, such as {@link
+     * FlowExpressions.MethodCall}, {@link FlowExpressions.ArrayAccess}, {@link
+     * FlowExpressions.LocalVariable}, etc.
+     *
+     * @see <a href="https://checkerframework.org/manual/#java-expressions-as-arguments">the syntax
+     *     of Java expressions supported by the Checker Framework</a>
      */
     public abstract static class Receiver {
         /** The type of this expression. */

docs/manual/advanced-features.tex

@@ -1140,7 +1140,9 @@
 \item \refqualclass{checker/lock/qual}{Holding}
 \end{itemize}
 
-The set of permitted expressions is a subset of all Java expressions:
+The set of permitted expressions is a subset of all Java expressions,
+with a few extensions, formal parameters like \<\#1> and (for some type
+systems) \code{<self>}.
 
 \begin{itemize}
 \item
@@ -1246,20 +1248,12 @@
 
 
 \textbf{Limitations:}
-The following Java expressions may not currently be written:
-% The Checker Framework is best at reasoning about Java expressions that
-% are variable references, but these expressions are not.
-\begin{itemize}
-\item String concatenation expressions.
-\item Mathematical operators (plus, minus, division, ...).
-\item Comparisons (equality, less than, etc.).
-\end{itemize}
-
-Additionally, it is not possible to write
-quantification over all array components (e.g. to express that all
+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.
 
+
 \sectionAndLabel{Field invariants}{field-invariants}
 
 Sometimes a field declared in a superclass has a more precise type in a