This is important for handling certain JDK cases like Class.isArray(), which if it returns true, ensures that getComponentType() on the same object returns @NonNull:
https://github.com/typetools/jdk/blob/9b1958333ddd472b31fa9ad6cc1b7faf80edd664/src/java.base/share/classes/java/lang/Class.java#L844
Not modeling this leads to a lot of false positives on JUnit (with JSpecify JDK models enabled). There's a similar relationship between Queue.isEmpty() and Queue.peek() / Queue.poll(), though modeling that is more complex since a Queue can contain nulls and also isEmpty() is inherited from Collection.
This is important for handling certain JDK cases like
Class.isArray(), which if it returns true, ensures thatgetComponentType()on the same object returns@NonNull:https://github.com/typetools/jdk/blob/9b1958333ddd472b31fa9ad6cc1b7faf80edd664/src/java.base/share/classes/java/lang/Class.java#L844
Not modeling this leads to a lot of false positives on JUnit (with JSpecify JDK models enabled). There's a similar relationship between
Queue.isEmpty()andQueue.peek()/Queue.poll(), though modeling that is more complex since aQueuecan contain nulls and alsoisEmpty()is inherited fromCollection.