Add receiver refinement in getAnnotatedTypeLhs

framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java

@@ -1657,9 +1657,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) {
      */
     public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
         AnnotatedTypeMirror res;
-        boolean oldUseFlow = useFlow;
         boolean oldShouldCache = shouldCache;
-        useFlow = false;
         // Don't cache the result because getAnnotatedType(lhsTree) could
         // be called from elsewhere and would expect flow-sensitive type refinements.
         shouldCache = false;
@@ -1668,6 +1666,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
             case IDENTIFIER:
             case MEMBER_SELECT:
             case ARRAY_ACCESS:
+                // For member-select tree, we want the receiver to have the refinement
                 res = getAnnotatedType(lhsTree);
                 break;
             case PARENTHESIZED:
@@ -1687,7 +1686,6 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
                                     + lhsTree.getKind());
                 }
         }
-        useFlow = oldUseFlow;
         shouldCache = oldShouldCache;
         return res;
     }

framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java

@@ -1,4 +1,4 @@
-package tests;
+package org.checkerframework.framework.test.junit;
 
 import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
 import org.junit.runners.Parameterized;

framework/tests/viewpointtest/TestGetAnnotatedLhs.java

@@ -0,0 +1,35 @@
+import viewpointtest.quals.A;
+import viewpointtest.quals.B;
+import viewpointtest.quals.ReceiverDependentQual;
+import viewpointtest.quals.Top;
+
+@ReceiverDependentQual
+class TestGetAnnotatedLhs {
+    @ReceiverDependentQual Object f;
+
+    @SuppressWarnings({
+        "inconsistent.constructor.type",
+        "super.invocation.invalid",
+        "cast.unsafe.constructor.invocation"
+    })
+    @ReceiverDependentQual
+    TestGetAnnotatedLhs() {
+        this.f = new @ReceiverDependentQual Object();
+    }
+
+    @SuppressWarnings({"cast.unsafe.constructor.invocation"})
+    void topWithRefinement() {
+        TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs();
+        TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
+        top = a;
+        // :: error: (assignment.type.incompatible)
+        top.f = new @B Object();
+        top.f = new @A Object(); // no error here
+    }
+
+    @SuppressWarnings({"cast.unsafe.constructor.invocation"})
+    void topWithoutRefinement() {
+        TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs();
+        top.f = new @A Object();
+    }
+}