diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index f6bb92176527..d40fa1e682bb 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/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; } diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java index 1c98b6552bb1..b602eb2fb22c 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java +++ b/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; diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java new file mode 100644 index 000000000000..4e9da8cc411f --- /dev/null +++ b/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(); + } +}