diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index d85f0814579..e62afd33dce 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -8,6 +8,7 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.plumelib.util.IPair; @@ -285,7 +286,12 @@ protected AnnotatedTypeMirror combineAnnotationWithType( AnnotatedTypeMirror resLower = combineAnnotationWithType(receiverAnnotation, atv.getLowerBound()); mappings.put(atv.getLowerBound(), resLower); - + // The values of the mappings are the viewpoint adapted lower and upper bounds, + // and we wish to replace the old bounds of atv with the new mappings. + // However, we need to first remove the primary annotations of atv, otherwise + // in later replacement, the primary annotations would override our computed + // new mappings (see method fixupBoundAnnotations). + atv.clearAnnotations(); AnnotatedTypeMirror result = AnnotatedTypeCopierWithReplacement.replace(atv, mappings); @@ -408,6 +414,25 @@ private AnnotatedTypeMirror substituteTVars(AnnotatedTypeMirror lhs, AnnotatedTy // Base case where actual type argument is extracted if (lhs.getKind() == TypeKind.DECLARED) { rhs = getTypeVariableSubstitution((AnnotatedDeclaredType) lhs, atv); + // When substituting an annotated type variable use (e.g., fields, return type), we + // don't want to replace the type qualifier of it with the qualifier on the + // type argument, as specified in + // https://checkerframework.org/manual/#type-variable-use. However, method + // getTypeVariableSubstitution will replace the annotated type qualifier as well. + // We fix up the substitution by checking if the types of the lower and upper bound + // are the same. If they are the same: (1) either the type variable use is + // annotated, and we need to fix up the + // primary annotation of the substituted result (rhs) by replacing it with the + // previous annotated type qualifier (from atv); (2) or the use is not annotated, + // but + // the type parameter is declared with the same upper and lower bounds, and it's no + // harm doing the same replacement as (1) because the qualifiers of the substituted + // result (rhs) and the old type variable use (atv) must be the same. + if (AnnotationUtils.areSame( + atv.getLowerBound().getAnnotations(), + atv.getUpperBound().getAnnotations())) { + rhs.replaceAnnotations(atv.getLowerBound().getAnnotations()); + } } } else if (rhs.getKind() == TypeKind.DECLARED) { AnnotatedDeclaredType adt = (AnnotatedDeclaredType) rhs.shallowCopy(); diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java new file mode 100644 index 00000000000..c71c97abf3b --- /dev/null +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -0,0 +1,17 @@ +import viewpointtest.quals.*; + +@SuppressWarnings("cast.unsafe.constructor.invocation") +class AnnoOnTypeVariableUse { + @ReceiverDependentQual E element; + + static void test() { + AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<@B Element>(); + // d.element = @A |> @RDQ = @A + // thus expects no error here + d.element = new @A Element(); + } +} + +class Element { + int f = 1; +}