Nullness postconditions for String#equals and String#equalsIgnoreCase

[GoogleCodeExporter]

The attached patch adds nullness post-conditions for java.lang.String#equals 
and String#equalsIgnoreCase. This is sound because:

- These methods are implemented such that an argument of 'null' causes the 
method to return false
- String is a final class, so the implementation of these methods cannot be 
overridden by subclasses

Original issue reported on code.google.com by atomknig...@gmail.com on 4 Dec 2014 at 1:32

Attachments:

• String_equals_nullness_postcondition.patch

[GoogleCodeExporter]

I concur.  Thanks, Abraham, for the annotations!

I have pushed this change:  
https://code.google.com/p/checker-framework/source/detail?r=b9370914aa59c6bd39e4
3dd9b2ddbc96fba9c151

Actually, every equals method should be annotated as you indicated.  We don't 
want to clutter up the annotated libraries with them, however.  The proposed 
fix is noted in issue 286, issue 334, and issue 342.  In the meanwhile, adding 
these annotations is fine.

Original comment by mer...@cs.washington.edu on 4 Dec 2014 at 6:19

• Changed state: Pushed

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 20 Dec 2014 at 2:16

• Changed state: Fixed