biddyweb / checker-framework

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

Bogus Warning with @EnsuresNonNull (postcondition not satisfied) #372

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
What steps will reproduce the problem?
1. Run the Null Checker on the class below
import java.util.HashMap;
import java.util.Map;

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.KeyFor;

class Test {
    private final Map<String, String> labels = new HashMap<>();

    @EnsuresNonNull("labels.get(#1)")
    void foo(@KeyFor("labels") String v) {
        labels.put(v, "");
    }
}

What is the expected output? What do you see instead?
Expected: No warning
Actual: Warning: the postcondition about 'this.labels.get(v)' of this method is 
not satisfied void foo(@KeyFor("labels") String v) {

What version of the product are you using? On what operating system?
1.8.6/Windows 8/Java 8

Original issue reported on code.google.com by ClovisSe...@gmail.com on 4 Oct 2014 at 10:48

GoogleCodeExporter commented 9 years ago
I have reproduced this error and created the test case: 
checker/tests/nullness/Issue372.java

Original comment by mcart...@cs.washington.edu on 19 Nov 2014 at 10:04

GoogleCodeExporter commented 9 years ago

Original comment by mcart...@cs.washington.edu on 19 Nov 2014 at 11:14

GoogleCodeExporter commented 9 years ago

Original comment by mcart...@cs.washington.edu on 19 Nov 2014 at 11:15