Add a checker to handle the contract of the JDK's binary search method

[kelloggm]

Fixes kelloggm#121 (modulo samelen bugs).

Doing this as a checker made the most sense, because we want the information to be available to both the lower and upper bound checkers.

[smillst]

@kelloggm should I review this?

[mernst]

@smillst I believe there are still outstanding issues from my review. You can probably wait until someone assigns it to you.

[kelloggm]

I've resolved the issues identified by Mike in his review. @smillst, it should be ready for you.

[mernst]

It's up to the reviewer, not the reviewee, to decide whether the changes are adequate.

There are often issues that the reviewer didn't get to -- maybe they didn't make sense but will in the context of better code or comments.

[kelloggm]

Did I imply otherwise? My impression from your previous comment was that I should assign it to Suzanne when I thought I had addressed your concerns. I can reassign it to you instead if you want to review it again (or I was just mistaken in how I interpreted what you said).

[mernst]

In general, a PR should be reviewed by one person at a time. It's usually more efficient to do reviews sequentially rather than in parallel. Changing the reviewer is a pretty aggressive tactic that says you don't consider the original one useful.

[kelloggm]

My apologies, then. That's not what I intended at all; I thought you'd given me blessing to do so.

[mernst]

Sorry, on my side, for writing a comment that was open to misinterpretation.

[kelloggm]

No worries! As long as everyone had good intentions, there's no problem.

[kelloggm]

@mernst I think I've addressed your feedback.

[mernst]

Please double-check that the tests pass before re-assigning the pull request. (I fixed the failure, Ithink.) Could you expand the type hierarchy figure in the manual to include an example of @SearchIndexFor and one of @NegativeIndexFor with multiple arguments?

[kelloggm]

@smillst I've explicitly implemented lub and glb, and the NPE from the all-systems/Issue1006.java went away. It should now be ready for your review.

Unrelated, the travis build seems to be failing because the JDK isn't being built first. I'm not sure why this happens, but someone with knowledge of the build system should probably look into it. The two failing test lines (SearchIndexTests.java, lines 7 and 10) are both values derived from calling binary search that should be properly assigned by the JDK (with a pre-built JDK on my machine, the tests pass, and the only reason they would fail is if the JDK did not have the proper annotations - they literally check if the annotations on the JDK method are correct).

[smillst]

The travis build seems to be failing because the JDK isn't being built first.

See checker-framework/.travis.yml. You can change whether or not Travis builds the jdk during testing in that file. I made it to that in https://github.com/typetools/checker-framework/pull/1182/commits/f9a03f1f2a9cb6c29e6c07b0dd6712dcbf85d58b. Make sure you revert that change before merging. (Actually, I'll need to remake the jdk that Travis uses to include these annotations before you merge.)

[kelloggm]

@smillst I've made LUB and GLB more precise. I think they were sound overapproximations before, and that they're now as precise as they can be. Sorry I forgot that case.

[smillst]

I made a version of the jdk.jars with the new annotations and changed the build to download it. (See https://github.com/typetools/checker-framework/pull/1182/commits/1ac7671f94fc30121f5ad94839511d0587f5081a#diff-8e6f9ff3c77d439c1733f5fd5fe2bb6bR1437) That will need to be reverted before merging. But hopefully the tests will now pass.

[kelloggm]

@smillst I think this is ready to be merged. Is there anything else that needs to be addressed? If not, I can remove the JDK things and merge.