lovubuntu / checker-framework

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

@KeyFor handles shadowed map name incorrectly #273

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
The following code throws a java.lang.NullPointerException, despite it being 
verified by the CF Nullness Checker. The problem is that the KeyFor map name 
refers to something different in getMap2 than in main.

import checkers.nullness.quals.*;
import java.util.Map;
import java.util.HashMap;

class A {
    public static void main(String... p) {
        Map<String, Integer> m0 = new HashMap<String,Integer>();
        Map<String, Integer> m1 = new HashMap<String,Integer>();
        @SuppressWarnings("assignment.type.incompatible")
        @KeyFor("m0") String k = "key";
        m0.put(k, 1);

        getMap2(m0,m1,k).toString();
    }

    public static @NonNull Integer getMap2(
            Map<String, Integer> m1,  // m1,m0 flipped
            Map<String, Integer> m0, 
            @KeyFor("m0") String k) 
    {
        return m0.get(k);
    }
}

Original issue reported on code.google.com by weitz...@cs.washington.edu on 16 Nov 2013 at 12:25

GoogleCodeExporter commented 9 years ago
Thanks for the bug report.
I have committed your test case as
checkers/tests/nullness/KeyForShadowing.java

Original comment by michael.ernst@gmail.com on 16 Nov 2013 at 2:34

GoogleCodeExporter commented 9 years ago

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