ThreadLocal and nullable types

[Jon Schewe]

Why is ThreadLocal annotated as NonNull rather than allowing the user of the class to specify if the value can be null or not?

https://github.com/checklt/checklt/blob/master/checker-framework/checkers/jdk/nullness/src/java/lang/ThreadLocal.java

[Jo D]

I assume it's because the nullness checker wants @NonNull to be the default (for reasons).

What I don't know:

• Why it was explicitly annotated.
• Why you have to suppress a warning; that sounds as if the inference rules of the nullness checker have inconsistencies or omissions (but that may just be the novice in me speaking).

[Michael Ernst]

Jo-

I'm sorry, but I don't understand your question.  You ask "why it was explicitly annotated", but you linked to a file that contains no explicit `@NonNull` annotation.  You linked not to the Checker Framework repository, but to what seems to be a copy of a rather old version of the Checker Framework.  You also didn't state any problem that you are having.

Could you please open an issue, showing the client code that you are having trouble verifying?

Thanks,

Mike

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/281f1798-f4da-4544-b498-47c3f510ca88n%40googlegroups.com.

[Jo D]

Hi Michael,

The source code link was posted by Jon Schewe, who was trying to figure out what the copy of ThreadLocal.java he was seeing wanted to tell him.

I have no problem with ThreadLocal myself, I was trying to answer his question to the best of my abilities ;-)

Though I do now have the question where we mere mortals can figure out what the effective annotations on some JDK class are?

Regards,

Jo

[Jon Schewe]

Michael,

Here is the proper reference https://github.com/typetools/jdk/blob/master/src/java.base/share/classes/java/lang/ThreadLocal.java#L84

Sorry for the incorrect reference the first time.

This explicit annotation of Nullable for the type of ThreadLocal does not allow one to have objects that are guaranteed to be NonNull inside a ThreadLocal object. Is the reason for the Nullable parameter type because the default implementation of initialValue is null? 

Jo, this repository is where you can find all of the annotations in the annotated JDK that is shipped with checker.

Jon Schewe

[Jon Schewe]

I spent some more time digging into this tonight. I expect that the fact that the default implementation of initialValue returns null means that the Nullable annotation must exist.

It seems that those writing the JDK should have made ThreadLocal be an abstract class. That would have fixed this and kept a lot of people from making mistakes by not overriding the initialValue method.

However given that I see that https://github.com/typetools/checker-framework/issues/1572 is open to define a MustOverride annotation, which seems like a reasonable work around for APIs that choose not to use abstract classes.

I did get the warning suppression to work, but found that the one in the comment is incorrect. I opened https://github.com/typetools/checker-framework/issues/4708 to have that fixed.

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/checker-framework-discuss/342dfad75125964d9f966fb25e5fa89d45e99c63.camel%40mtu.net.