From 13e16979e16663326591edba5f795bee84ef51e8 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 3 Aug 2024 13:27:57 -0400 Subject: [PATCH 01/22] Add lost qualifier --- .../ViewpointTestAnnotatedTypeFactory.java | 2 ++ .../ViewpointTestViewpointAdapter.java | 10 ++++++++-- .../src/test/java/viewpointtest/quals/Bottom.java | 2 +- .../src/test/java/viewpointtest/quals/Lost.java | 15 +++++++++++++++ .../tests/viewpointtest/TestGetAnnotatedLhs.java | 4 ++-- 5 files changed, 28 insertions(+), 5 deletions(-) create mode 100644 framework/src/test/java/viewpointtest/quals/Lost.java diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index f2027bae843..7d851cdf267 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -10,6 +10,7 @@ import viewpointtest.quals.A; import viewpointtest.quals.B; import viewpointtest.quals.Bottom; +import viewpointtest.quals.Lost; import viewpointtest.quals.PolyVP; import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; @@ -29,6 +30,7 @@ protected Set> createSupportedTypeQualifiers() { Bottom.class, PolyVP.class, ReceiverDependentQual.class, + Lost.class, Top.class); } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index 9da9504eead..e93ba9349fa 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -8,12 +8,13 @@ import javax.lang.model.element.AnnotationMirror; +import viewpointtest.quals.Lost; import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { - private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL; + private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, LOST; /** * The class constructor. @@ -26,6 +27,7 @@ public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) { RECEIVERDEPENDENTQUAL = AnnotationBuilder.fromClass( atypeFactory.getElementUtils(), ReceiverDependentQual.class); + LOST = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), Lost.class); } @Override @@ -38,7 +40,11 @@ protected AnnotationMirror combineAnnotationWithAnnotation( AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) { if (AnnotationUtils.areSame(declaredAnnotation, RECEIVERDEPENDENTQUAL)) { - return receiverAnnotation; + if (AnnotationUtils.areSame(receiverAnnotation, TOP)) { + return LOST; + } else { + return receiverAnnotation; + } } return declaredAnnotation; } diff --git a/framework/src/test/java/viewpointtest/quals/Bottom.java b/framework/src/test/java/viewpointtest/quals/Bottom.java index 484726ae7f4..753d57fad71 100644 --- a/framework/src/test/java/viewpointtest/quals/Bottom.java +++ b/framework/src/test/java/viewpointtest/quals/Bottom.java @@ -13,6 +13,6 @@ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -@SubtypeOf({A.class, B.class, ReceiverDependentQual.class}) +@SubtypeOf({A.class, B.class, ReceiverDependentQual.class, Top.class, PolyVP.class, Lost.class}) @DefaultFor(TypeUseLocation.LOWER_BOUND) public @interface Bottom {} diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java new file mode 100644 index 00000000000..d77ef725db4 --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -0,0 +1,15 @@ +package viewpointtest.quals; + +import org.checkerframework.framework.qual.SubtypeOf; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({Top.class}) +public @interface Lost {} diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index 71641a91a71..fb44dae8e8a 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java @@ -36,9 +36,9 @@ void topWithRefinement() { @SuppressWarnings({"cast.unsafe.constructor.invocation"}) void topWithoutRefinement() { TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); - // See #576. - // :TODO: error: (assignment.type.incompatible) + // :: error: (assignment.type.incompatible) top.f = new @B Object(); + // :: error: (assignment.type.incompatible) top.f = new @A Object(); } } From 0364e47f26a46ad99060124bb8af3641c12c177c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sat, 3 Aug 2024 19:48:16 -0400 Subject: [PATCH 02/22] Add error message for Top receiver method invocation --- framework/tests/viewpointtest/VPAExamples.java | 2 ++ framework/tests/viewpointtest/VarargsConstructor.java | 5 +++++ 2 files changed, 7 insertions(+) diff --git a/framework/tests/viewpointtest/VPAExamples.java b/framework/tests/viewpointtest/VPAExamples.java index 65312090d7d..396febd003f 100644 --- a/framework/tests/viewpointtest/VPAExamples.java +++ b/framework/tests/viewpointtest/VPAExamples.java @@ -30,7 +30,9 @@ void tests(@A RDContainer a, @B RDContainer b, @Top RDContainer top) { // :: error: (argument.type.incompatible) b.set(aObj); b.set(bObj); + // :: error: (argument.type.incompatible) top.set(aObj); + // :: error: (argument.type.incompatible) top.set(bObj); } } diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index acf2380d741..6fdb35e6c94 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/framework/tests/viewpointtest/VarargsConstructor.java @@ -17,6 +17,7 @@ void foo() { void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { @A Object a = new @A VarargsConstructor(aObj); @B Object b = new @B VarargsConstructor(bObj); + // :: error: (argument.type.incompatible) @Top Object top = new @Top VarargsConstructor(topObj); // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj); @@ -31,14 +32,17 @@ class Inner { void foo() { Inner a = new Inner(); + // :: error: (argument.type.incompatible) Inner b = new Inner(new Object()); Inner c = VarargsConstructor.this.new Inner(); + // :: error: (argument.type.incompatible) Inner d = VarargsConstructor.this.new Inner(new Object()); } void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { @A Object a = new @A Inner(aObj); @B Object b = new @B Inner(bObj); + // :: error: (argument.type.incompatible) @Top Object top = new @Top Inner(topObj); // :: error: (argument.type.incompatible) new @A Inner(bObj); @@ -56,6 +60,7 @@ void foo() { }; @A Object a = new @A VarargsConstructor(aObj) {}; @B Object b = new @B VarargsConstructor(bObj) {}; + // :: error: (argument.type.incompatible) @Top Object top = new @Top VarargsConstructor(topObj) {}; // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj) {}; From c859999fbdaf05a2d08df318d5efe9559489ec03 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 12 Aug 2024 00:23:06 -0400 Subject: [PATCH 03/22] Implement lost is not reflexive by overriding the subtype rules --- .../ViewpointTestAnnotatedTypeFactory.java | 7 ++++ .../ViewpointTestQualifierHierarchy.java | 40 +++++++++++++++++++ .../tests/viewpointtest/LostNonReflexive.java | 37 +++++++++++++++++ 3 files changed, 84 insertions(+) create mode 100644 framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java create mode 100644 framework/tests/viewpointtest/LostNonReflexive.java diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index 7d851cdf267..c96f0ca66df 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -3,6 +3,7 @@ import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.type.AbstractViewpointAdapter; +import org.checkerframework.framework.type.QualifierHierarchy; import java.lang.annotation.Annotation; import java.util.Set; @@ -38,4 +39,10 @@ protected Set> createSupportedTypeQualifiers() { protected AbstractViewpointAdapter createViewpointAdapter() { return new ViewpointTestViewpointAdapter(this); } + + @Override + public QualifierHierarchy createQualifierHierarchy() { + return new ViewpointTestQualifierHierarchy( + this.getSupportedTypeQualifiers(), elements, this); + } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java new file mode 100644 index 00000000000..44268ef540c --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java @@ -0,0 +1,40 @@ +package viewpointtest; + +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.type.NoElementQualifierHierarchy; + +import java.lang.annotation.Annotation; +import java.util.Collection; + +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.util.Elements; + +import viewpointtest.quals.Bottom; +import viewpointtest.quals.Lost; + +/** A qualifier hierarchy for the ViewpointTest checker. */ +public class ViewpointTestQualifierHierarchy extends NoElementQualifierHierarchy { + /** + * Creates a ViewpointTestQualifierHierarchy from the given classes. + * + * @param qualifierClasses classes of annotations that are the qualifiers + * @param elements element utils + * @param atypeFactory the associated type factory + */ + public ViewpointTestQualifierHierarchy( + Collection> qualifierClasses, + Elements elements, + GenericAnnotatedTypeFactory atypeFactory) { + super(qualifierClasses, elements, atypeFactory); + } + + @Override + public boolean isSubtypeQualifiers(AnnotationMirror subAnno, AnnotationMirror superAnno) { + // Lost is not reflexive and the only subtype is Bottom + if (atypeFactory.areSameByClass(superAnno, Lost.class) + && !atypeFactory.areSameByClass(subAnno, Bottom.class)) { + return false; + } + return super.isSubtypeQualifiers(subAnno, superAnno); + } +} diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java new file mode 100644 index 00000000000..17a7887b362 --- /dev/null +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -0,0 +1,37 @@ +import viewpointtest.quals.*; + +public class LostNonReflexive { + @ReceiverDependentQual Object f; + + @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + @ReceiverDependentQual + LostNonReflexive(@ReceiverDependentQual Object args) {} + + @ReceiverDependentQual + Object get() { + return null; + } + + void set(@ReceiverDependentQual Object o) {} + + void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { + // :: error: (assignment.type.incompatible) + this.f = obj.f; + this.f = bottomObj; + + // :: error: (assignment.type.incompatible) + @A Object aObj = obj.get(); + // :: error: (assignment.type.incompatible) + @B Object bObj = obj.get(); + // :: error: (assignment.type.incompatible) + @Bottom Object botObj = obj.get(); + + // :: error: (argument.type.incompatible) + new LostNonReflexive(obj.f); + new LostNonReflexive(bottomObj); + + // :: error: (argument.type.incompatible) + this.set(obj.f); + this.set(bottomObj); + } +} From 36905fbee76d9fd2610518416b3a2798f1d1eccb Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 12 Aug 2024 16:30:25 -0400 Subject: [PATCH 04/22] Empty commit for CI From 270c933453c54af43bb3b0e493de4ad3d99fcaac Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Tue, 20 Aug 2024 10:36:14 -0400 Subject: [PATCH 05/22] Correct format for Javadoc Co-authored-by: Werner Dietl --- .../java/viewpointtest/ViewpointTestQualifierHierarchy.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java index 44268ef540c..c3a5bf28647 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java @@ -12,7 +12,7 @@ import viewpointtest.quals.Bottom; import viewpointtest.quals.Lost; -/** A qualifier hierarchy for the ViewpointTest checker. */ +/** A qualifier hierarchy for the Viewpoint Test Checker. */ public class ViewpointTestQualifierHierarchy extends NoElementQualifierHierarchy { /** * Creates a ViewpointTestQualifierHierarchy from the given classes. From 4151fce1797c394e933d59e918e4123cb4f7e47a Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 20 Aug 2024 10:38:58 -0400 Subject: [PATCH 06/22] Add link to QualifierHierarchy class --- .../java/viewpointtest/ViewpointTestQualifierHierarchy.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java index c3a5bf28647..df40405dfaf 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java @@ -12,7 +12,7 @@ import viewpointtest.quals.Bottom; import viewpointtest.quals.Lost; -/** A qualifier hierarchy for the Viewpoint Test Checker. */ +/** The {@link QualifierHierarchy} for the Viewpoint Test Checker. */ public class ViewpointTestQualifierHierarchy extends NoElementQualifierHierarchy { /** * Creates a ViewpointTestQualifierHierarchy from the given classes. From 744acc69a641c4c3b59a49e4272bfdde45b5c440 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 21 Aug 2024 21:20:49 -0400 Subject: [PATCH 07/22] Fix javadoc link --- .../test/java/viewpointtest/ViewpointTestQualifierHierarchy.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java index df40405dfaf..e76c54ea61c 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java @@ -2,6 +2,7 @@ import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; import org.checkerframework.framework.type.NoElementQualifierHierarchy; +import org.checkerframework.framework.type.QualifierHierarchy; import java.lang.annotation.Annotation; import java.util.Collection; From c879d468f396b077df530234b9fb3af9de63b62a Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 8 Sep 2024 11:40:06 -0400 Subject: [PATCH 08/22] Add missing error message --- framework/tests/viewpointtest/SuperConstructorCalls.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index cf7213d6e9f..cf58484bf86 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/framework/tests/viewpointtest/SuperConstructorCalls.java @@ -18,6 +18,7 @@ public Inner() { } public Inner(@Top Object objTop) { + // :: error: (argument.type.incompatible) super(objTop); } From 2a1f9a28684fca05300d384770a52ebf67b6804e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 8 Sep 2024 12:06:20 -0400 Subject: [PATCH 09/22] Add javadoc --- .../java/viewpointtest/ViewpointTestViewpointAdapter.java | 2 ++ framework/src/test/java/viewpointtest/quals/Lost.java | 7 +++++++ 2 files changed, 9 insertions(+) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index b6c54da1647..133d5626c49 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -12,8 +12,10 @@ import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; +/** The viewpoint adapter for the ViewpointTest checker. */ public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { + /** The {@link Top}, {@link ReceiverDependentQual} and {@Lost} annotation. */ private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, LOST; /** diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index d77ef725db4..e12cc514802 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -8,6 +8,13 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; +/** + * {@link Lost} is type annotation that indicates the relationship can not be expressed. It is the + * result of viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. + * + *

It is not reflexive in subtyping relationship and the only subtype for {@link Lost} is {@link + * Bottom}. + */ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) From 1be71d0125a9e78bb4468f3abbefc32b448c7bde Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Sun, 8 Sep 2024 13:17:18 -0400 Subject: [PATCH 10/22] Fix Javadoc --- .../test/java/viewpointtest/ViewpointTestViewpointAdapter.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index 133d5626c49..41fecb64fe9 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -15,7 +15,7 @@ /** The viewpoint adapter for the ViewpointTest checker. */ public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { - /** The {@link Top}, {@link ReceiverDependentQual} and {@Lost} annotation. */ + /** The {@link Top}, {@link ReceiverDependentQual} and {@link Lost} annotation. */ private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, LOST; /** From ed98bf0d98141969767dc9236aa55a32c5dc2cbe Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Wed, 2 Oct 2024 22:35:26 -0400 Subject: [PATCH 11/22] Wording Co-authored-by: Werner Dietl --- framework/src/test/java/viewpointtest/quals/Lost.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index e12cc514802..e4c7b72b905 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -9,10 +9,10 @@ import java.lang.annotation.Target; /** - * {@link Lost} is type annotation that indicates the relationship can not be expressed. It is the + * The {@link Lost} qualifier indicates that a relationship cannot be expressed. It is the * result of viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. * - *

It is not reflexive in subtyping relationship and the only subtype for {@link Lost} is {@link + *

It is not reflexive in the subtyping relationship and the only subtype for {@link Lost} is {@link * Bottom}. */ @Documented From b9cf1db32b4575bdca665f1285f63bbae80f8965 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 2 Oct 2024 22:48:06 -0400 Subject: [PATCH 12/22] Comment for viewpoint adapta super call --- framework/tests/viewpointtest/SuperConstructorCalls.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index cf58484bf86..1de85793045 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/framework/tests/viewpointtest/SuperConstructorCalls.java @@ -17,6 +17,9 @@ public Inner() { super(); } + // The constructor's return type is implicitly @Top by default. + // When calling the super constructor, @Top becomes @Lost in the super constructor's signature, + // causing a type mismatch with the expected @ReceiverDependentQual parameter. public Inner(@Top Object objTop) { // :: error: (argument.type.incompatible) super(objTop); From a070489d7f159e1edd3064afa54c42a77724817f Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 2 Oct 2024 22:48:22 -0400 Subject: [PATCH 13/22] Format --- framework/tests/viewpointtest/SuperConstructorCalls.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/tests/viewpointtest/SuperConstructorCalls.java b/framework/tests/viewpointtest/SuperConstructorCalls.java index 1de85793045..fc0e5a66f83 100644 --- a/framework/tests/viewpointtest/SuperConstructorCalls.java +++ b/framework/tests/viewpointtest/SuperConstructorCalls.java @@ -18,8 +18,8 @@ public Inner() { } // The constructor's return type is implicitly @Top by default. - // When calling the super constructor, @Top becomes @Lost in the super constructor's signature, - // causing a type mismatch with the expected @ReceiverDependentQual parameter. + // When calling the super constructor, @Top becomes @Lost in the super constructor's + // signature, causing a type mismatch with the expected @ReceiverDependentQual parameter. public Inner(@Top Object objTop) { // :: error: (argument.type.incompatible) super(objTop); From bf37ee96649d6264e2200e38b8e5ce63b2286733 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 3 Oct 2024 00:45:29 -0400 Subject: [PATCH 14/22] Move `new.class.type.invalid` to basetype's error message --- .../org/checkerframework/checker/nullness/messages.properties | 1 - .../org/checkerframework/common/basetype/messages.properties | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties index f1ccf838bf4..e3aaa1a85d3 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/nullness/messages.properties @@ -22,7 +22,6 @@ nulltest.redundant=redundant test against null; "%s" is non-null instanceof.nullable=instanceof is only true for a non-null expression instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof new.array.type.invalid=annotations %s may not be applied as component type for array "%s" -new.class.type.invalid=the annotations %s do not need be applied in object creations nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null nullness.on.enum=do not write nullness annotations on an enum constant, which is always non-null nullness.on.exception.parameter=do not write nullness annotations on an exception parameter, which is always non-null diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index 1644fa2acdb..357f4b03036 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -2,6 +2,7 @@ receiver.invalid=incompatible types.%nfound : %s%nrequired: %s type.anno.before.modifier=write type annotation %s immediately before type, after modifiers %s type.anno.before.decl.anno=write type annotations %s immediately before type, after declaration annotation %s +new.class.type.invalid=the annotations %s do not need be applied in object creations array.initializer.type.incompatible=incompatible types in array initializer.%nfound : %s%nrequired: %s assignment.type.incompatible=incompatible types in assignment.%nfound : %s%nrequired: %s From c27c02dffc5f6d060fdb9a4d0295561e71e2d2c9 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 3 Oct 2024 00:46:14 -0400 Subject: [PATCH 15/22] Forbid create `@top` Object --- .../ViewpointTestAnnotatedTypeFactory.java | 6 +++++ .../viewpointtest/ViewpointTestVisitor.java | 23 ++++++++++++++++ .../test/java/viewpointtest/quals/Lost.java | 8 +++--- .../tests/viewpointtest/PolyConstructor.java | 3 ++- .../viewpointtest/TestGetAnnotatedLhs.java | 2 ++ .../viewpointtest/VarargsConstructor.java | 26 ++++++++++++------- 6 files changed, 53 insertions(+), 15 deletions(-) create mode 100644 framework/src/test/java/viewpointtest/ViewpointTestVisitor.java diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index c96f0ca66df..1e4f1acb3b9 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -4,10 +4,13 @@ import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.type.AbstractViewpointAdapter; import org.checkerframework.framework.type.QualifierHierarchy; +import org.checkerframework.javacutil.AnnotationBuilder; import java.lang.annotation.Annotation; import java.util.Set; +import javax.lang.model.element.AnnotationMirror; + import viewpointtest.quals.A; import viewpointtest.quals.B; import viewpointtest.quals.Bottom; @@ -18,6 +21,9 @@ public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { + /** The {@link Top} annotation. */ + public final AnnotationMirror TOP = AnnotationBuilder.fromClass(elements, Top.class); + public ViewpointTestAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker); this.postInit(); diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java new file mode 100644 index 00000000000..8a7308c20c7 --- /dev/null +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -0,0 +1,23 @@ +package viewpointtest; + +import com.sun.source.tree.NewClassTree; + +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.common.basetype.BaseTypeVisitor; +import org.checkerframework.framework.type.AnnotatedTypeMirror; + +public class ViewpointTestVisitor extends BaseTypeVisitor { + + public ViewpointTestVisitor(BaseTypeChecker checker) { + super(checker); + } + + @Override + public Void visitNewClass(NewClassTree tree, Void p) { + AnnotatedTypeMirror Type = atypeFactory.getAnnotatedType(tree); + if (Type.hasAnnotation(atypeFactory.TOP)) { + checker.reportError(tree, "new.class.type.invalid", Type.getAnnotations()); + } + return super.visitNewClass(tree, p); + } +} diff --git a/framework/src/test/java/viewpointtest/quals/Lost.java b/framework/src/test/java/viewpointtest/quals/Lost.java index e4c7b72b905..ade8ff1d01b 100644 --- a/framework/src/test/java/viewpointtest/quals/Lost.java +++ b/framework/src/test/java/viewpointtest/quals/Lost.java @@ -9,11 +9,11 @@ import java.lang.annotation.Target; /** - * The {@link Lost} qualifier indicates that a relationship cannot be expressed. It is the - * result of viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. + * The {@link Lost} qualifier indicates that a relationship cannot be expressed. It is the result of + * viewpoint adaptation that combines {@link Top} and {@link ReceiverDependentQual}. * - *

It is not reflexive in the subtyping relationship and the only subtype for {@link Lost} is {@link - * Bottom}. + *

It is not reflexive in the subtyping relationship and the only subtype for {@link Lost} is + * {@link Bottom}. */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/framework/tests/viewpointtest/PolyConstructor.java b/framework/tests/viewpointtest/PolyConstructor.java index 766a874b014..d829420283c 100644 --- a/framework/tests/viewpointtest/PolyConstructor.java +++ b/framework/tests/viewpointtest/PolyConstructor.java @@ -6,7 +6,8 @@ static class MyClass { @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) @PolyVP MyClass(@PolyVP Object o) { - throw new RuntimeException(" * You are filled with DETERMINATION."); // stub + // :: warning: (cast.unsafe.constructor.invocation) + throw new @A RuntimeException(" * You are filled with DETERMINATION."); // stub } } diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index fb44dae8e8a..7bbeb447e95 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java @@ -20,6 +20,7 @@ class TestGetAnnotatedLhs { @SuppressWarnings({"cast.unsafe.constructor.invocation"}) void topWithRefinement() { TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs(); + // :: error: (new.class.type.invalid) TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); top = a; // When checking the below assignment, GenericAnnotatedTypeFactory#getAnnotatedTypeLhs() @@ -35,6 +36,7 @@ void topWithRefinement() { @SuppressWarnings({"cast.unsafe.constructor.invocation"}) void topWithoutRefinement() { + // :: error: (new.class.type.invalid) TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); // :: error: (assignment.type.incompatible) top.f = new @B Object(); diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index 6fdb35e6c94..26dc48f87a4 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/framework/tests/viewpointtest/VarargsConstructor.java @@ -11,13 +11,14 @@ public class VarargsConstructor { VarargsConstructor(@ReceiverDependentQual Object... args) {} void foo() { - VarargsConstructor a = new VarargsConstructor("testStr", new Object()); + // :: warning: (cast.unsafe.constructor.invocation) + VarargsConstructor a = new @A VarargsConstructor("testStr", new @A Object()); } void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { @A Object a = new @A VarargsConstructor(aObj); @B Object b = new @B VarargsConstructor(bObj); - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) @Top Object top = new @Top VarargsConstructor(topObj); // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj); @@ -32,17 +33,19 @@ class Inner { void foo() { Inner a = new Inner(); - // :: error: (argument.type.incompatible) - Inner b = new Inner(new Object()); + // :: error: (argument.type.incompatible) :: warning: + // (cast.unsafe.constructor.invocation) + Inner b = new Inner(new @A Object()); Inner c = VarargsConstructor.this.new Inner(); - // :: error: (argument.type.incompatible) - Inner d = VarargsConstructor.this.new Inner(new Object()); + // :: error: (argument.type.incompatible) :: warning: + // (cast.unsafe.constructor.invocation) + Inner d = VarargsConstructor.this.new Inner(new @A Object()); } void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { @A Object a = new @A Inner(aObj); @B Object b = new @B Inner(bObj); - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) @Top Object top = new @Top Inner(topObj); // :: error: (argument.type.incompatible) new @A Inner(bObj); @@ -53,14 +56,17 @@ void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { void testAnonymousClass(@A Object aObj, @B Object bObj, @Top Object topObj) { Object o = - new VarargsConstructor("testStr", new Object()) { + // :: warning: (cast.unsafe.constructor.invocation) + new @A VarargsConstructor("testStr", new @A Object()) { void foo() { - VarargsConstructor a = new VarargsConstructor("testStr", new Object()); + VarargsConstructor a = + // :: warning: (cast.unsafe.constructor.invocation) + new @A VarargsConstructor("testStr", new @A Object()); } }; @A Object a = new @A VarargsConstructor(aObj) {}; @B Object b = new @B VarargsConstructor(bObj) {}; - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) @Top Object top = new @Top VarargsConstructor(topObj) {}; // :: error: (argument.type.incompatible) new @A VarargsConstructor(bObj) {}; From c56f67f82cea18ac5affd6bb518b41564c1fce1b Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 3 Oct 2024 11:52:47 -0400 Subject: [PATCH 16/22] Javadoc --- .../viewpointtest/ViewpointTestAnnotatedTypeFactory.java | 6 ++++++ .../src/test/java/viewpointtest/ViewpointTestVisitor.java | 7 ++++++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index 1e4f1acb3b9..d54f87fd17a 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -19,11 +19,17 @@ import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; +/** The annotated type factory for the viewpointtest type-system. */ public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { /** The {@link Top} annotation. */ public final AnnotationMirror TOP = AnnotationBuilder.fromClass(elements, Top.class); + /** + * Create a new ViewpointTestAnnotatedTypeFactory. + * + * @param checker the checker to which this annotated type factory belongs + */ public ViewpointTestAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker); this.postInit(); diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 8a7308c20c7..b80c8900ed6 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -6,8 +6,13 @@ import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; +/** The visitor for the viewpointtest type-system. */ public class ViewpointTestVisitor extends BaseTypeVisitor { - + /** + * Create a new ViewpointTestVisitor. + * + * @param checker the checker to which this visitor belongs + */ public ViewpointTestVisitor(BaseTypeChecker checker) { super(checker); } From 8fd343372492f4695a557e97ac0abe7cd1601b7f Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 9 Oct 2024 12:23:54 -0400 Subject: [PATCH 17/22] Apply spotless --- framework/tests/viewpointtest/LostNonReflexive.java | 6 ++---- framework/tests/viewpointtest/PolyConstructor.java | 1 - 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index 17a7887b362..770baadfbca 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -4,11 +4,9 @@ public class LostNonReflexive { @ReceiverDependentQual Object f; @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) - @ReceiverDependentQual - LostNonReflexive(@ReceiverDependentQual Object args) {} + @ReceiverDependentQual LostNonReflexive(@ReceiverDependentQual Object args) {} - @ReceiverDependentQual - Object get() { + @ReceiverDependentQual Object get() { return null; } diff --git a/framework/tests/viewpointtest/PolyConstructor.java b/framework/tests/viewpointtest/PolyConstructor.java index 8fa68709f2b..66ab42c48d9 100644 --- a/framework/tests/viewpointtest/PolyConstructor.java +++ b/framework/tests/viewpointtest/PolyConstructor.java @@ -4,7 +4,6 @@ public class PolyConstructor { static class MyClass { @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) - @PolyVP MyClass(@PolyVP Object o) { throw new RuntimeException(" * You are filled with DETERMINATION."); // stub } From b0db749b0698757ce2dc8db56ee47603bd21ee9e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 9 Oct 2024 12:26:46 -0400 Subject: [PATCH 18/22] Adapt test to new changes --- framework/tests/viewpointtest/PolyConstructor.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/framework/tests/viewpointtest/PolyConstructor.java b/framework/tests/viewpointtest/PolyConstructor.java index 66ab42c48d9..5cb60fd9f06 100644 --- a/framework/tests/viewpointtest/PolyConstructor.java +++ b/framework/tests/viewpointtest/PolyConstructor.java @@ -3,9 +3,10 @@ public class PolyConstructor { static class MyClass { - @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + // :: error: (super.invocation.invalid) :: warning: (inconsistent.constructor.type) @PolyVP MyClass(@PolyVP Object o) { - throw new RuntimeException(" * You are filled with DETERMINATION."); // stub + // :: warning: (cast.unsafe.constructor.invocation) + throw new @A RuntimeException(" * You are filled with DETERMINATION."); // stub } } From 3970bbc0933bd0332d4e3a99350dad09d10d50e1 Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Wed, 13 Nov 2024 15:33:30 -0800 Subject: [PATCH 19/22] Consistent Javadoc Co-authored-by: Werner Dietl --- .../java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java | 2 +- .../java/viewpointtest/ViewpointTestQualifierHierarchy.java | 2 +- .../test/java/viewpointtest/ViewpointTestViewpointAdapter.java | 2 +- framework/src/test/java/viewpointtest/ViewpointTestVisitor.java | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index d54f87fd17a..bdb484cb5d8 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -19,7 +19,7 @@ import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; -/** The annotated type factory for the viewpointtest type-system. */ +/** The annotated type factory for the Viewpoint Test Checker. */ public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { /** The {@link Top} annotation. */ diff --git a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java index e76c54ea61c..b5dfaed769a 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestQualifierHierarchy.java @@ -31,7 +31,7 @@ public ViewpointTestQualifierHierarchy( @Override public boolean isSubtypeQualifiers(AnnotationMirror subAnno, AnnotationMirror superAnno) { - // Lost is not reflexive and the only subtype is Bottom + // Lost is not reflexive and the only subtype is Bottom. if (atypeFactory.areSameByClass(superAnno, Lost.class) && !atypeFactory.areSameByClass(subAnno, Bottom.class)) { return false; diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index 41fecb64fe9..8694d1522d9 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -12,7 +12,7 @@ import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; -/** The viewpoint adapter for the ViewpointTest checker. */ +/** The viewpoint adapter for the Viewpoint Test Checker. */ public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { /** The {@link Top}, {@link ReceiverDependentQual} and {@link Lost} annotation. */ diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index b80c8900ed6..3e8e8e98e77 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -6,7 +6,7 @@ import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; -/** The visitor for the viewpointtest type-system. */ +/** The visitor for the Viewpoint Test Checker. */ public class ViewpointTestVisitor extends BaseTypeVisitor { /** * Create a new ViewpointTestVisitor. From 0fd471e8cc2bf3df90524249c6d08907940bf23e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 13 Nov 2024 16:47:12 -0800 Subject: [PATCH 20/22] Address comment and update with more test cases --- .../common/basetype/messages.properties | 2 +- .../ViewpointTestAnnotatedTypeFactory.java | 3 +++ .../viewpointtest/ViewpointTestVisitor.java | 2 +- .../tests/viewpointtest/LostNonReflexive.java | 3 ++- .../tests/viewpointtest/PolyConstructor.java | 27 ++++++++++++++++++- .../viewpointtest/VarargsConstructor.java | 15 +++++------ 6 files changed, 40 insertions(+), 12 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index 357f4b03036..87fcc85c9ac 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -2,7 +2,6 @@ receiver.invalid=incompatible types.%nfound : %s%nrequired: %s type.anno.before.modifier=write type annotation %s immediately before type, after modifiers %s type.anno.before.decl.anno=write type annotations %s immediately before type, after declaration annotation %s -new.class.type.invalid=the annotations %s do not need be applied in object creations array.initializer.type.incompatible=incompatible types in array initializer.%nfound : %s%nrequired: %s assignment.type.incompatible=incompatible types in assignment.%nfound : %s%nrequired: %s @@ -35,6 +34,7 @@ cast.unsafe.constructor.invocation=constructor invocation cast from "%s" to "%s" exception.parameter.invalid=invalid type in exception parameter.%nfound : %s%nrequired: %s throw.type.invalid=invalid type thrown.%nfound : %s%nrequired: %s expression.unparsable.type.invalid=Expression invalid in dependent type annotation: %s +new.class.type.invalid=type annotation %s can not be applied to object creation explicit.annotation.ignored=The qualifier %s is ignored in favor of %s. Either delete %s or change it to %s. override.return.invalid=Incompatible return type.%nfound : %s%nrequired: %s%nConsequence: method in %s%n %s%ncannot override method in %s%n %s diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index bdb484cb5d8..a17426e754a 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -25,6 +25,9 @@ public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory /** The {@link Top} annotation. */ public final AnnotationMirror TOP = AnnotationBuilder.fromClass(elements, Top.class); + /** The {@link Lost} annotation. */ + public final AnnotationMirror LOST = AnnotationBuilder.fromClass(elements, Lost.class); + /** * Create a new ViewpointTestAnnotatedTypeFactory. * diff --git a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java index 3e8e8e98e77..928860b199d 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestVisitor.java @@ -20,7 +20,7 @@ public ViewpointTestVisitor(BaseTypeChecker checker) { @Override public Void visitNewClass(NewClassTree tree, Void p) { AnnotatedTypeMirror Type = atypeFactory.getAnnotatedType(tree); - if (Type.hasAnnotation(atypeFactory.TOP)) { + if (Type.hasAnnotation(atypeFactory.TOP) || Type.hasAnnotation(atypeFactory.LOST)) { checker.reportError(tree, "new.class.type.invalid", Type.getAnnotations()); } return super.visitNewClass(tree, p); diff --git a/framework/tests/viewpointtest/LostNonReflexive.java b/framework/tests/viewpointtest/LostNonReflexive.java index 770baadfbca..eacc4c9b132 100644 --- a/framework/tests/viewpointtest/LostNonReflexive.java +++ b/framework/tests/viewpointtest/LostNonReflexive.java @@ -24,8 +24,9 @@ void test(@Top LostNonReflexive obj, @Bottom Object bottomObj) { // :: error: (assignment.type.incompatible) @Bottom Object botObj = obj.get(); - // :: error: (argument.type.incompatible) + // :: error: (argument.type.incompatible) :: error: (new.class.type.invalid) new LostNonReflexive(obj.f); + // :: error: (new.class.type.invalid) new LostNonReflexive(bottomObj); // :: error: (argument.type.incompatible) diff --git a/framework/tests/viewpointtest/PolyConstructor.java b/framework/tests/viewpointtest/PolyConstructor.java index 5cb60fd9f06..eec0533b8ae 100644 --- a/framework/tests/viewpointtest/PolyConstructor.java +++ b/framework/tests/viewpointtest/PolyConstructor.java @@ -5,8 +5,33 @@ public class PolyConstructor { static class MyClass { // :: error: (super.invocation.invalid) :: warning: (inconsistent.constructor.type) @PolyVP MyClass(@PolyVP Object o) { + // :: error: (new.class.type.invalid) + throw new RuntimeException(" * You are filled with DETERMINATION."); // stub + } + + void throwTopException() { + // :: error: (new.class.type.invalid) + throw new @Top RuntimeException(); + } + + void throwBottomException() { + // :: warning: (cast.unsafe.constructor.invocation) + throw new @Bottom RuntimeException(); + } + + void throwAException() { + // :: warning: (cast.unsafe.constructor.invocation) + throw new @A RuntimeException(); + } + + void throwBException() { // :: warning: (cast.unsafe.constructor.invocation) - throw new @A RuntimeException(" * You are filled with DETERMINATION."); // stub + throw new @B RuntimeException(); + } + + void throwLostException() { + // :: error: (new.class.type.invalid) :: warning: (cast.unsafe.constructor.invocation) + throw new @Lost RuntimeException(); } } diff --git a/framework/tests/viewpointtest/VarargsConstructor.java b/framework/tests/viewpointtest/VarargsConstructor.java index 7b18284d461..bacd874f592 100644 --- a/framework/tests/viewpointtest/VarargsConstructor.java +++ b/framework/tests/viewpointtest/VarargsConstructor.java @@ -26,18 +26,17 @@ void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { } class Inner { - @SuppressWarnings({"inconsistent.constructor.type", "super.invocation.invalid"}) + // :: warning: (inconsistent.constructor.type) :: error:(super.invocation.invalid) @ReceiverDependentQual Inner(@ReceiverDependentQual Object... args) {} void foo() { + // :: error: (new.class.type.invalid) Inner a = new Inner(); - // :: error: (argument.type.incompatible) :: warning: - // (cast.unsafe.constructor.invocation) - Inner b = new Inner(new @A Object()); - Inner c = VarargsConstructor.this.new Inner(); - // :: error: (argument.type.incompatible) :: warning: - // (cast.unsafe.constructor.invocation) - Inner d = VarargsConstructor.this.new Inner(new @A Object()); + // :: warning: (cast.unsafe.constructor.invocation) + Inner b = new @A Inner(new @A Object()); + Inner c = VarargsConstructor.this.new @A Inner(); + // :: warning: (cast.unsafe.constructor.invocation) + Inner d = VarargsConstructor.this.new @A Inner(new @A Object()); } void invokeConstructor(@A Object aObj, @B Object bObj, @Top Object topObj) { From 4326a192835919d97013178ac77de4c010b00ba2 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Wed, 4 Dec 2024 17:38:57 -0500 Subject: [PATCH 21/22] Don't recreate the same qualifiers --- .../java/viewpointtest/ViewpointTestViewpointAdapter.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index 8694d1522d9..f9f9d76f1f1 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -25,11 +25,11 @@ public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { */ public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); - TOP = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), Top.class); + TOP = atypeFactory.TOP; RECEIVERDEPENDENTQUAL = AnnotationBuilder.fromClass( atypeFactory.getElementUtils(), ReceiverDependentQual.class); - LOST = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), Lost.class); + LOST = atypeFactory.LOST; } @Override From bbc07c1ec86d55eaae0970520f42e45c3070e9d0 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Thu, 5 Dec 2024 20:22:53 -0500 Subject: [PATCH 22/22] Add downcasts --- .../java/viewpointtest/ViewpointTestViewpointAdapter.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index f9f9d76f1f1..aae61833e10 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -25,11 +25,11 @@ public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { */ public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) { super(atypeFactory); - TOP = atypeFactory.TOP; + TOP = ((ViewpointTestAnnotatedTypeFactory) atypeFactory).TOP; RECEIVERDEPENDENTQUAL = AnnotationBuilder.fromClass( atypeFactory.getElementUtils(), ReceiverDependentQual.class); - LOST = atypeFactory.LOST; + LOST = ((ViewpointTestAnnotatedTypeFactory) atypeFactory).LOST; } @Override