From 6a9379826020a596ae9e208485dd9eced656b9bd Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 23 Mar 2026 14:52:58 -0400 Subject: [PATCH 01/10] Report type arguments in method invocation --- .../MethodReceiverTypeErrorMessageTest.java | 20 +++++++++++++++++++ .../MethodReceiverTypeErrorMessageTest.out | 7 +++++++ .../common/basetype/BaseTypeVisitor.java | 12 +++++------ 3 files changed, 33 insertions(+), 6 deletions(-) create mode 100644 checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java create mode 100644 checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out diff --git a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java new file mode 100644 index 000000000000..bdadce691358 --- /dev/null +++ b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java @@ -0,0 +1,20 @@ +/* + * @test + * @summary Test case for method receiver type in error message. If it is a non-raw type, it should be printed as such. + * + * @compile/fail/ref=MethodReceiverTypeErrorMessageTest.out -XDrawDiagnostics -processor org.checkerframework.checker.nullness.NullnessChecker MethodReceiverTypeErrorMessageTest.java + */ +public class MethodReceiverTypeErrorMessageTest { + + MethodReceiverTypeErrorMessageTest() { + foo(); + } + + void foo() {} +} + +class sub extends MethodReceiverTypeErrorMessageTest { + sub() { + foo(); + } +} diff --git a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out new file mode 100644 index 000000000000..be305e0cf630 --- /dev/null +++ b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out @@ -0,0 +1,7 @@ +MethodReceiverTypeErrorMessageTest.java:10:12: compiler.err.proc.messager: [method.invocation.invalid] call to foo() not allowed on the given receiver. +found : @UnderInitialization(MethodReceiverTypeErrorMessageTest.class) MethodReceiverTypeErrorMessageTest +required: @Initialized MethodReceiverTypeErrorMessageTest +MethodReceiverTypeErrorMessageTest.java:18:12: compiler.err.proc.messager: [method.invocation.invalid] call to foo() not allowed on the given receiver. +found : @UnderInitialization(sub.class) sub +required: @Initialized MethodReceiverTypeErrorMessageTest<@Initialized String> +2 errors \ No newline at end of file diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 4bdeda3ca0b8..7b434baa0bf6 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3983,19 +3983,19 @@ protected void checkMethodInvocability( return; } - AnnotatedTypeMirror erasedMethodReceiver = method.getReceiverType().getErased(); - AnnotatedTypeMirror erasedTreeReceiver = erasedMethodReceiver.shallowCopy(false); + AnnotatedTypeMirror methodReceiver = method.getReceiverType(); + AnnotatedTypeMirror erasedTreeReceiver = methodReceiver.shallowCopy(false); AnnotatedTypeMirror treeReceiver = atypeFactory.getReceiverType(tree); erasedTreeReceiver.addAnnotations(treeReceiver.getEffectiveAnnotations()); - if (!skipReceiverSubtypeCheck(tree, erasedMethodReceiver, treeReceiver)) { + if (!skipReceiverSubtypeCheck(tree, methodReceiver, treeReceiver)) { // The diagnostic can be a bit misleading because the check is of the receiver but // `tree` is the entire method invocation (where the receiver might be implicit). - commonAssignmentCheckStartDiagnostic(erasedMethodReceiver, erasedTreeReceiver, tree); - boolean success = typeHierarchy.isSubtype(erasedTreeReceiver, erasedMethodReceiver); + commonAssignmentCheckStartDiagnostic(methodReceiver, erasedTreeReceiver, tree); + boolean success = typeHierarchy.isSubtype(erasedTreeReceiver, methodReceiver); commonAssignmentCheckEndDiagnostic( - success, null, erasedMethodReceiver, erasedTreeReceiver, tree); + success, null, methodReceiver, erasedTreeReceiver, tree); if (!success) { // Don't report the erased types because they show up with '' as type args. reportMethodInvocabilityError(tree, treeReceiver, method.getReceiverType()); From 520fd92b1fc2b7e43c60408a13f87d4b2613b73a Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 23 Mar 2026 16:19:59 -0400 Subject: [PATCH 02/10] Empty line at the end --- checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out index be305e0cf630..8ebbd6ab47d4 100644 --- a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out +++ b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out @@ -4,4 +4,4 @@ required: @Initialized MethodReceiverTypeErrorMessageTest -2 errors \ No newline at end of file +2 errors From e12bb14d0a024d98e2ae99b80a1195865f3a62d0 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 11:37:05 -0400 Subject: [PATCH 03/10] Improve test case --- .../nullness/MethodReceiverTypeErrorMessageTest.java | 8 ++++---- .../jtreg/nullness/MethodReceiverTypeErrorMessageTest.out | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java index bdadce691358..5728c2f2d409 100644 --- a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java +++ b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.java @@ -11,10 +11,10 @@ public class MethodReceiverTypeErrorMessageTest { } void foo() {} -} -class sub extends MethodReceiverTypeErrorMessageTest { - sub() { - foo(); + static class StringSpecialization extends MethodReceiverTypeErrorMessageTest { + StringSpecialization() { + foo(); + } } } diff --git a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out index 8ebbd6ab47d4..6c2c97e29eac 100644 --- a/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out +++ b/checker/jtreg/nullness/MethodReceiverTypeErrorMessageTest.out @@ -1,7 +1,7 @@ MethodReceiverTypeErrorMessageTest.java:10:12: compiler.err.proc.messager: [method.invocation.invalid] call to foo() not allowed on the given receiver. found : @UnderInitialization(MethodReceiverTypeErrorMessageTest.class) MethodReceiverTypeErrorMessageTest required: @Initialized MethodReceiverTypeErrorMessageTest -MethodReceiverTypeErrorMessageTest.java:18:12: compiler.err.proc.messager: [method.invocation.invalid] call to foo() not allowed on the given receiver. -found : @UnderInitialization(sub.class) sub +MethodReceiverTypeErrorMessageTest.java:17:16: compiler.err.proc.messager: [method.invocation.invalid] call to foo() not allowed on the given receiver. +found : @UnderInitialization(MethodReceiverTypeErrorMessageTest.StringSpecialization.class) StringSpecialization required: @Initialized MethodReceiverTypeErrorMessageTest<@Initialized String> 2 errors From 317d1ce7c195437231c5c55787ba3232c53df353 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 11:38:13 -0400 Subject: [PATCH 04/10] Call 'getErased' --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 7b434baa0bf6..dcd0c127ec1d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3984,7 +3984,7 @@ protected void checkMethodInvocability( } AnnotatedTypeMirror methodReceiver = method.getReceiverType(); - AnnotatedTypeMirror erasedTreeReceiver = methodReceiver.shallowCopy(false); + AnnotatedTypeMirror erasedTreeReceiver = methodReceiver.shallowCopy(false).getErased(); AnnotatedTypeMirror treeReceiver = atypeFactory.getReceiverType(tree); erasedTreeReceiver.addAnnotations(treeReceiver.getEffectiveAnnotations()); From 5e7619f5e4f98d2790be99afd087cf23cc36ed2c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 11:42:04 -0400 Subject: [PATCH 05/10] Changelog --- docs/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 58c433a1a7ce..aefd16c26db2 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,8 @@ Version 3.49.5-eisop1 (July ??, 2025) **User-visible changes:** +Method invocation mismatch diagnostics now report exact receiver type arguments instead of printing raw types. + The new command-line option `-AonlyAnnotatedFor` suppresses all type-checking errors and warnings outside the scope of a corresponding `@AnnotatedFor` annotation. Note that the `@AnnotatedFor` annotation must include the checker's name to enable warnings from that checker. @@ -37,7 +39,6 @@ They are enabled by default and can be disabled using `-Alint=-instanceof.unsafe The Nullness Checker now recognizes references to private, final fields with zero-length arrays as initializers in calls to `Collection.toArray(T[])`, allowing the returned component type to be refined to `@NonNull`. The `ClassBound` annotation can now be used with anonymous types. - **Implementation details:** The `AbstractNodeVisitor` now has more summary methods, following the class hierarchy of `Node` and conceptual categories. From 27fe900e51359c177223f6ecc110309f49654a18 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 12:32:23 -0400 Subject: [PATCH 06/10] Revert --- docs/CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index aefd16c26db2..833b2101f00e 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -39,6 +39,7 @@ They are enabled by default and can be disabled using `-Alint=-instanceof.unsafe The Nullness Checker now recognizes references to private, final fields with zero-length arrays as initializers in calls to `Collection.toArray(T[])`, allowing the returned component type to be refined to `@NonNull`. The `ClassBound` annotation can now be used with anonymous types. + **Implementation details:** The `AbstractNodeVisitor` now has more summary methods, following the class hierarchy of `Node` and conceptual categories. From f71ed77fea7cbb11ef6d69b08ef7e27a30fec921 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 19:40:13 -0400 Subject: [PATCH 07/10] Apply suggestion from @wmdietl Co-authored-by: Werner Dietl --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index dcd0c127ec1d..e681e146b637 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3984,7 +3984,7 @@ protected void checkMethodInvocability( } AnnotatedTypeMirror methodReceiver = method.getReceiverType(); - AnnotatedTypeMirror erasedTreeReceiver = methodReceiver.shallowCopy(false).getErased(); + AnnotatedTypeMirror erasedTreeReceiver = methodReceiver.getErased().shallowCopy(false); AnnotatedTypeMirror treeReceiver = atypeFactory.getReceiverType(tree); erasedTreeReceiver.addAnnotations(treeReceiver.getEffectiveAnnotations()); From 70a355bfe39ae42361c78a1a59835695050ea5e2 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 19:44:25 -0400 Subject: [PATCH 08/10] Use the variable already defined --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index e681e146b637..6cc07475f687 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3998,7 +3998,7 @@ protected void checkMethodInvocability( success, null, methodReceiver, erasedTreeReceiver, tree); if (!success) { // Don't report the erased types because they show up with '' as type args. - reportMethodInvocabilityError(tree, treeReceiver, method.getReceiverType()); + reportMethodInvocabilityError(tree, treeReceiver, methodReceiver); } } } From 37942c12b970431eb4a70dfaf0c9bb714d39c0c3 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 20:44:54 -0400 Subject: [PATCH 09/10] Revert changes and use full type the diagnostic --- docs/CHANGELOG.md | 2 -- .../common/basetype/BaseTypeVisitor.java | 15 ++++++++------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 833b2101f00e..58c433a1a7ce 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,8 +3,6 @@ Version 3.49.5-eisop1 (July ??, 2025) **User-visible changes:** -Method invocation mismatch diagnostics now report exact receiver type arguments instead of printing raw types. - The new command-line option `-AonlyAnnotatedFor` suppresses all type-checking errors and warnings outside the scope of a corresponding `@AnnotatedFor` annotation. Note that the `@AnnotatedFor` annotation must include the checker's name to enable warnings from that checker. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6cc07475f687..87b6a016839d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3983,22 +3983,23 @@ protected void checkMethodInvocability( return; } - AnnotatedTypeMirror methodReceiver = method.getReceiverType(); - AnnotatedTypeMirror erasedTreeReceiver = methodReceiver.getErased().shallowCopy(false); + AnnotatedTypeMirror erasedMethodReceiver = method.getReceiverType().getErased(); + AnnotatedTypeMirror erasedTreeReceiver = erasedMethodReceiver.shallowCopy(false); AnnotatedTypeMirror treeReceiver = atypeFactory.getReceiverType(tree); erasedTreeReceiver.addAnnotations(treeReceiver.getEffectiveAnnotations()); - if (!skipReceiverSubtypeCheck(tree, methodReceiver, treeReceiver)) { + if (!skipReceiverSubtypeCheck(tree, erasedMethodReceiver, treeReceiver)) { // The diagnostic can be a bit misleading because the check is of the receiver but // `tree` is the entire method invocation (where the receiver might be implicit). - commonAssignmentCheckStartDiagnostic(methodReceiver, erasedTreeReceiver, tree); - boolean success = typeHierarchy.isSubtype(erasedTreeReceiver, methodReceiver); + commonAssignmentCheckStartDiagnostic( + method.getReceiverType(), erasedTreeReceiver, tree); + boolean success = typeHierarchy.isSubtype(erasedTreeReceiver, erasedMethodReceiver); commonAssignmentCheckEndDiagnostic( - success, null, methodReceiver, erasedTreeReceiver, tree); + success, null, method.getReceiverType(), erasedTreeReceiver, tree); if (!success) { // Don't report the erased types because they show up with '' as type args. - reportMethodInvocabilityError(tree, treeReceiver, methodReceiver); + reportMethodInvocabilityError(tree, treeReceiver, method.getReceiverType()); } } } From f84a6616fa6e2f0869822301d4a7105273f87c6f Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 24 Mar 2026 21:21:47 -0400 Subject: [PATCH 10/10] Introduce local variable --- .../common/basetype/BaseTypeVisitor.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 87b6a016839d..c9a256fa866f 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3983,7 +3983,8 @@ protected void checkMethodInvocability( return; } - AnnotatedTypeMirror erasedMethodReceiver = method.getReceiverType().getErased(); + AnnotatedTypeMirror methodReceiver = method.getReceiverType(); + AnnotatedTypeMirror erasedMethodReceiver = methodReceiver.getErased(); AnnotatedTypeMirror erasedTreeReceiver = erasedMethodReceiver.shallowCopy(false); AnnotatedTypeMirror treeReceiver = atypeFactory.getReceiverType(tree); @@ -3992,14 +3993,13 @@ protected void checkMethodInvocability( if (!skipReceiverSubtypeCheck(tree, erasedMethodReceiver, treeReceiver)) { // The diagnostic can be a bit misleading because the check is of the receiver but // `tree` is the entire method invocation (where the receiver might be implicit). - commonAssignmentCheckStartDiagnostic( - method.getReceiverType(), erasedTreeReceiver, tree); + commonAssignmentCheckStartDiagnostic(methodReceiver, erasedTreeReceiver, tree); boolean success = typeHierarchy.isSubtype(erasedTreeReceiver, erasedMethodReceiver); commonAssignmentCheckEndDiagnostic( - success, null, method.getReceiverType(), erasedTreeReceiver, tree); + success, null, methodReceiver, erasedTreeReceiver, tree); if (!success) { // Don't report the erased types because they show up with '' as type args. - reportMethodInvocabilityError(tree, treeReceiver, method.getReceiverType()); + reportMethodInvocabilityError(tree, treeReceiver, methodReceiver); } } }