Experience with @DefaultQualifier?

[Michael Ernst]

Does anyone use the @DefaultQualifier annotation?
If so, what is your experience with it?
Does it save a lot of annotations?
Is it confusing because two identically-annotated types mean different
things based on a far-removed @DefaultQualifier annotation?

Recall that the DefaultQualifier annotation
(http://types.cs.washington.edu/checker-framework/doc/checkers/quals/DefaultQualifier.html)
lets you set the default qualifier for a given package, class, method, or
variable. For example, you could set the default in one package to be
@NonNull, and the default in another package to be @Nullable.

I'm asking because I suspect that @DefaultQualifier is a
frequently-requested, but rarely-used, feature. I hypothesize that
@DefaultQualifier is generally obviated by good defaults (like the Nullness
Checker's "non-null except locals" default) and by type inference within
method bodies. This has been the experience of users I have talked with.

However, I would like to hear from more users. We'll continue to support
@DefaultQualifier, no matter what the outcome of the discussion, but it
will be nice to have a fact-based assessment of its usefulness. Such an
assessment can be gained only via use in practice.

Thanks!

-Mike

[Michael Ernst]

From the lack of response, it appears that the built-in defaults do the
right thing most of the time, so there is little need for
@DefaultQualifier.

However, I have found one use for @DefaultQualifier. Suppose that you are
using the Nullness Checker to type-check a class whose public interface
is supposed to accept any arguments whatsoever. Then, it can be expedient
to set the default to @Nullable. You may only want this default on method
parameters, not on fields, return values, and type parameters.

An example of such a class is JUnit's Assert class. It does have some
non-null formal parameters, such as the Matchers passed to assertThat(),
but most formal parameters are nullable. Every method in the class is
has void return type, and the class has no fields.

It seems that such examples are relatively rare, and so it is probably not
too much trouble to annotate the formal parameters of such libraries. If
anyone has other examples, send them along.

Thanks,

-Mike