Nullness Checker: support Q.isEmpty - Q.poll logic

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Use the attached code.
2. javac -processor org.checkerframework.checker.nullness.NullnessChecker 
-proc:only XX.java

What is the expected output? What do you see instead?

Should accept the code - but instead gives this error (which is wrong).
XX.java:41: error: [contracts.conditional.postcondition.not.satisfied] the 
conditional postcondition about 'this.popCheapest()' at this return statement 
is not satisfied
        return _pq.isEmpty();
        ^
1 error


What version of the product are you using? On what operating system?
1.8.10 / OSX

Please provide any additional information below.

Original issue reported on code.google.com by [email protected] on 12 Feb 2015 at 12:20

Attachments:

• XX.java