Ensures non null if return value is greater than zero

27 views
Skip to first unread message

Jon Schewe

unread,
Dec 18, 2021, 8:49:37 AM12/18/21
to Checker Framework discussion
I'm looking to annotate the method below to state that "cs" is not null if the return value is greater than zero. Is this possible with the checker framework?


  public static int length(final @Nullable CharSequence cs) {
    return cs == null ? 0 : cs.length();
  }

Michael Ernst

unread,
Dec 18, 2021, 9:12:33 AM12/18/21
to Jon Schewe, Checker Framework discussion
Jon-

This is not currently possible.  The Checker Framework could support such a rule, but the Nullness Checker is not currently integrated in this way with the Constant Value Checker or the Index Checker.

For any tool, there is some point at which programmers can be cleverer than the tool. :-)

                    -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/43d35522605c136dceae2bfbd357edb2fddea45f.camel%40mtu.net.
Reply all
Reply to author
Forward
0 new messages