Expand definition of local variable

checker/tests/nullness/java17/InstanceOfPatternVariable.java

@@ -0,0 +1,16 @@
+// @below-java17-jdk-skip-test
+// Test case for https://github.com/typetools/checker-framework/issues/5240
+
+import java.util.Map;
+import org.checkerframework.checker.nullness.qual.KeyFor;
+
+public class InstanceOfPatternVariable {
+
+  public void doSomething(final Object x) {
+    if (x instanceof Map<?, ?> m) {
+      // final var ct = (ClassOrInterfaceType) type;
+
+      @KeyFor("m") Object y = m.keySet().iterator().next();
+    }
+  }
+}

javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java

@@ -787,14 +787,14 @@ public static boolean isTypeDeclaration(Element elt) {
   /**
    * Return true if the element is a binding variable.
    *
-   * <p>Note: This is to conditionally support Java 15 instanceof pattern matching. When available,
-   * this should use {@code ElementKind.BINDING_VARIABLE} directly.
+   * <p>This implementation compiles under JDK 8 and 11 as well as versions that contain {@code
+   * ElementKind.BINDING_VARIABLE}.
    *
    * @param element the element to test
    * @return true if the element is a binding variable
    */
   public static boolean isBindingVariable(Element element) {
-    return "BINDING_VARIABLE".equals(element.getKind().name());
+    return SystemUtil.jreVersion >= 16 && "BINDING_VARIABLE".equals(element.getKind().name());
   }
 
   /**

javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java

@@ -245,11 +245,26 @@ public Env<AttrContext> getEnvForPath(TreePath path) {
     try {
       Env<AttrContext> env = getEnvForPath(path);
       Element res = wrapInvocationOnResolveInstance(FIND_VAR, env, names.fromString(name));
-      if (res.getKind() == ElementKind.LOCAL_VARIABLE || res.getKind() == ElementKind.PARAMETER) {
-        return (VariableElement) res;
-      } else {
-        // The Element might be FIELD or a SymbolNotFoundError.
-        return null;
+      // Every kind in the documentation of Element.getKind() is explicitly tested, possibly in the
+      // "default:" case.
+      switch (res.getKind()) {
+        case EXCEPTION_PARAMETER:
+        case LOCAL_VARIABLE:
+        case PARAMETER:
+        case RESOURCE_VARIABLE:
+          return (VariableElement) res;
+        case ENUM_CONSTANT:
+        case FIELD:
+          return null;
+        default:
+          if (ElementUtils.isBindingVariable(res)) {
+            return (VariableElement) res;
+          }
+          if (res instanceof VariableElement) {
+            throw new BugInCF("unhandled variable ElementKind " + res.getKind());
+          }
+          // The Element might be a SymbolNotFoundError.
+          return null;
       }
     } finally {
       log.popDiagnosticHandler(discardDiagnosticHandler);