Add receiver refinement in getAnnotatedTypeLhs

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

@@ -1626,6 +1626,15 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) {
         return type;
     }
 
+    @Override
+    public AnnotatedTypeMirror getAnnotatedType(Tree tree) {
+        boolean oldUseFlow = useFlow;
+        useFlow = everUseFlow;
+        AnnotatedTypeMirror res = super.getAnnotatedType(tree);
+        useFlow = oldUseFlow;
+        return res;
+    }
+
     /**
      * Returns the type of a left-hand side of an assignment.
      *
@@ -1648,7 +1657,8 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
             case IDENTIFIER:
             case MEMBER_SELECT:
             case ARRAY_ACCESS:
-                res = getAnnotatedType(lhsTree);
+                // For member-select tree, we want the receiver to have the refinement
+                res = super.getAnnotatedType(lhsTree);
                 break;
             case PARENTHESIZED:
                 res = getAnnotatedTypeLhs(TreeUtils.withoutParens((ExpressionTree) lhsTree));
@@ -1657,7 +1667,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
                 if (TreeUtils.isTypeTree(lhsTree)) {
                     // lhsTree is a type tree at the pseudo assignment of a returned expression to
                     // declared return type.
-                    res = getAnnotatedType(lhsTree);
+                    res = super.getAnnotatedType(lhsTree);
                 } else {
                     throw new BugInCF(
                             "GenericAnnotatedTypeFactory: Unexpected tree passed to"

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,28 @@
+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
+    Test() {
+        this.f = new @ReceiverDependentQual Object();
+    }
+
+    @SuppressWarnings({"cast.unsafe.constructor.invocation"})
+    void test1() {
+        Test a = new @A Test();
+        Test top = new @Top Test();
+        top = a;
+        // :: error: (assignment.type.incompatible)
+        top.f = new @B Object();
+    }
+}