lovubuntu / checker-framework

Automatically exported from code.google.com/p/checker-framework
0 stars 0 forks source link

Possibly incorrect nullness annotations on java.util.Properties#getProperty(String, String) #340

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago
Currently, the following is defined for 
java.util.Properties#getProperty(String, String):

    @Pure public @Nullable String getProperty(String a1, String a2) { throw new RuntimeException("skeleton method"); }

However, the OpenJDK implementation of that particular method looks like this:

    public String getProperty(String key, String defaultValue) {
        String val = getProperty(key);
        return (val == null) ? defaultValue : val;
    }

This suggests that the method might be better annotated as such:

    @Pure public @PolyNull String getProperty(String a1, @PolyNull String a2) { throw new RuntimeException("skeleton method"); }

Original issue reported on code.google.com by atomknig...@gmail.com on 14 Jul 2014 at 3:04

GoogleCodeExporter commented 9 years ago
Thanks for raising this issue.

This issue is a bit trickier than it looks at first glance.
The reason is that Properties is broken, due to poor design.

The proposed annotation is unsound if the property map contains null as a value.
Java makes no guarantee that the Properties object does not contain null as a 
value.
However, it is clear that the JDK designers intended that programmers should 
not put null in the Properties object.

A further wrinkle is that the implementation that you quoted does not conform 
to its specification.  The specification states, "The method returns the 
default value argument if the property is not found." but actually it returns 
the default value if the property is not found OR it has a null value.  Thus, 
assuming the OpenJDK implementation, the annotation really is sound.

So, there are two options:
 * retain the current annotation, which is sound but is unnecessarily conservative if clients use Properties in the way it is intended to be used
 * change the annotation as proposed, which is unsound if getProperty is reimplemented and if Properties is misused -- but which eliminates some false positives in the usual case

I am inclined toward the latter.  Although sacrificing soundness is generally 
an undesirable tradeoff, the risks seem low here.

Therefore, I have made the change.

java.lang.System.getProperty(String, String) already had the proposed @PolyNull 
annotation, so it did not need to be changed.

Original comment by michael.ernst@gmail.com on 19 Oct 2014 at 7:40

GoogleCodeExporter commented 9 years ago
Fixed in release 1.8.7

Original comment by Jonathan...@gmail.com on 30 Oct 2014 at 11:12