Nullness checker and built-in system properties

[GoogleCodeExporter]

Some Java system properties are built in; see 
  http://java.sun.com/javase/6/docs/api/java/lang/System.html#getProperties%28%29
For example, System.getProperty("line.separator") will never return null.

If the Nullness Checker recognized this, then users could avoid writing
warning suppressions for those cases.

A user can override the built-in values by doing something perverse like
   System.setProperty("line.separator", null);
Therefore, the checker should also forbid the following:
 * calling System.setProperties
 * calling System.setProperty or Properties.setProperty with:
    * a nullable value, and
    * argument a non-literal, or a literal that is any of the given strings
 * treating a Properties as a Hashtable.  This includes assigning to a
   variable of type Hashtable or calling any method that is inherited from
   Hashtable.  (It would probably be possible to slightly relax this
   condition, but it would be safe.)
With these conditions, if the whole program has been checked with the
Nullness Checker, then I believe the checking is still sound.

Original issue reported on code.google.com by michael.ernst@gmail.com on 12 Jul 2010 at 4:25

[GoogleCodeExporter]

A first version of this was pushed.

Original comment by wdi...@gmail.com on 15 Nov 2011 at 5:36

• Changed state: Pushed

[GoogleCodeExporter]

Thanks for the fixes.

Most problems are taken care of, in part because Properties extends 
Hashtable<...,@NonNull Object>.  However, it is still possible to remove a key 
from a Properties.  This can be done via 
checker-framework/checkers/tests/nullness/MisuseProperties.javaSystem.clearPrope
rty(), Properties.remove(), Properties.clear().

More problematically, it can also be done by treating a Properties as a 
Hashtable or Dictionary, then calling calling remove() or removeAll() or 
clear() or manipulating its keyset, valueset, or entryset.

I have added some test cases (not yet enabled), and some possible designs for 
sound checking, to file 
checker-framework/checkers/tests/nullness/MisuseProperties.java.  These are 
unsoundnesses, but perhaps relatively obscure ones.

Original comment by michael.ernst@gmail.com on 13 Sep 2012 at 4:56

• Changed state: Started
• Added labels: Priority-Low
• Removed labels: Priority-Medium