Open GoogleCodeExporter opened 9 years ago
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
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
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
Original issue reported on code.google.com by
rlen...@gmail.com
on 12 Feb 2015 at 12:20Attachments: