Limitation of Map Key checker with two containsKey checks

[GoogleCodeExporter]

The map key checker doesn't handle two containsKey tests performed together. Is 
this a known limitation?

Test case:

=== Test.java ===
import java.util.Map;

import org.checkerframework.checker.nullness.qual.*;

class Test {
  public static void m(Map<Object, Object> a, Map<Object, Object> b, Object ka, Object kb) {
    if (a.containsKey(ka)) {
      @NonNull Object i = a.get(ka); // OK
    }
    if (b.containsKey(kb)) {
      @NonNull Object i = b.get(kb); // OK
    }
    if (a.containsKey(ka) && b.containsKey(kb)) {
      @NonNull Object i = a.get(ka); // ERROR
      @NonNull Object j = b.get(kb); // ERROR
    }
  }
}
===

Output:

$  ~/jsr308/checker-framework-1.8.0/checker/bin/javac -version -processor 
org.checkerframework.checker.nullness.NullnessChecker -cp 
~/jsr308/checker-framework-1.8.0/checker/dist/checker-qual.jar Test.java
javac 1.8.0-jsr308-1.8.0
Test.java:14: error: [assignment.type.incompatible] incompatible types in 
assignment.
      @NonNull Object i = a.get(ka); // ERROR
                               ^
  found   : @Initialized @Nullable Object
  required: @UnknownInitialization @NonNull Object
Test.java:15: error: [assignment.type.incompatible] incompatible types in 
assignment.
      @NonNull Object j = b.get(kb); // ERROR
                               ^
  found   : @Initialized @Nullable Object
  required: @UnknownInitialization @NonNull Object
2 errors

Original issue reported on code.google.com by cus...@google.com on 3 May 2014 at 1:49

[GoogleCodeExporter]

Thanks for the bug report and example!
This is related to Issue 221: at the moment only certain heuristics are 
hard-coded for the map key checks. By re-implementing them as a dataflow 
analysis, more complex logic like in the example would be handled correctly.
cu, WMD.

Original comment by wdi...@gmail.com on 11 May 2014 at 6:27

• Changed state: Accepted

[GoogleCodeExporter]

Original comment by jtha...@cs.washington.edu on 17 Jul 2014 at 10:18

[GoogleCodeExporter]

This has been fixed.  I will add a test case for it.

Original comment by Jonathan...@gmail.com on 8 Apr 2015 at 10:30

• Changed state: Pushed