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 rlen...@gmail.com on 12 Feb 2015 at 12:20

Attachments:

• XX.java

[GoogleCodeExporter]

I don't see anything tying Queue#isEmpty or Queue#poll to the return value of 
popCheapest - this requires quite deep understanding of the code.

Original comment by wdi...@gmail.com on 17 Mar 2015 at 5:10

• Changed state: Invalid

[GoogleCodeExporter]

Sounds like perhaps a problem with the PQ annotations then - because Q.isEmpty 
returns false is the Q still has an element, and thus Q.poll returns a non-null 
element.

Original comment by rlen...@gmail.com on 17 Mar 2015 at 6:18

[GoogleCodeExporter]

Thanks for the comment, I see the point now.
I don't see this as a defect in @EnsuresNonNullIf, which does what it is 
supposed to. I changed the title accordingly.

I rather think we need additional logic to support the connection between 
Q.isEmpty and Q.poll, similarly to the connection between Map.get and 
Map.containsKey. None of the current pre/post-condition annotations is 
expressive enough to express such general logic. We will need something like

https://code.google.com/p/checker-framework/source/browse/checker/src/org/checke
rframework/checker/nullness/MapGetHeuristics.java

for Queues. (Note there is an updated version in our working repository right 
now.)

Original comment by wdi...@gmail.com on 17 Mar 2015 at 3:19

• Changed title: Nullness Checker: support Q.isEmpty - Q.poll logic
• Changed state: Accepted
• Added labels: Type-Enhancement
• Removed labels: Type-Defect