diff --git a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java index 1d8976036e1..97394dd83e5 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java @@ -1,7 +1,6 @@ package org.checkerframework.checker.index.samelen; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.qual.RelevantJavaTypes; import org.checkerframework.framework.source.SuppressWarningsPrefix; /** @@ -10,7 +9,9 @@ * * @checker_framework.manual #index-checker Index Checker */ -@RelevantJavaTypes({CharSequence.class, Object[].class, Object.class}) +// This @RelevantJavaTypes annotation is incorrect, because @SameLen can apply to an arbitrary +// user-defined datatype: https://checkerframework.org/manual/#index-annotating-fixed-size . +// @RelevantJavaTypes({CharSequence.class, Object[].class, Object.class}) @SuppressWarningsPrefix({"index", "samelen"}) public class SameLenChecker extends BaseTypeChecker { /** Create a new SameLenChecker. */ diff --git a/checker/tests/index/SameLenIrrelevant.java b/checker/tests/index/SameLenIrrelevant.java index b440dbaca30..c59ceefe46a 100644 --- a/checker/tests/index/SameLenIrrelevant.java +++ b/checker/tests/index/SameLenIrrelevant.java @@ -1,20 +1,24 @@ // Tests that adding an @SameLen annotation to a primitive type is still // an error. +// All the errors in this test case are disabled. They were issued when `@SameLen` was restricted +// to arrays and CharSequence, but @SameLen can be written on an arbitrary user-defined type: +// https://checkerframework.org/manual/#index-annotating-fixed-size . + import org.checkerframework.checker.index.qual.SameLen; public class SameLenIrrelevant { - // :: error: (anno.on.irrelevant) + // NO :: error: (anno.on.irrelevant) public void test(@SameLen("#2") int x, int y) { // do nothing } - // :: error: (anno.on.irrelevant) + // NO :: error: (anno.on.irrelevant) public void test(@SameLen("#2") double x, double y) { // do nothing } - // :: error: (anno.on.irrelevant) + // NO :: error: (anno.on.irrelevant) public void test(@SameLen("#2") char x, char y) { // do nothing }