Warning for when bounds declarations are not provably true.

[secure-sw-dev-bot]

This issue was copied from checkedc/checkedc-clang#343

---

This adds a warning message for when bounds declarations are not provably true. The warning is off by default because we cannot prove much yet about bounds declarations. This addresses work item #338.

We test the error message by adding checking of bounds declarations after assignments. We handle a few basic cases where the declared bounds for the target variable are implied by the inferred bounds of the source expression, that is a check for subsumption of bounds. Given e1 = e2, we allow the cases where:

• the declared bounds of e1 and inferred bounds of e2 are syntactically equal.
• the declared bounds of e1 is bounds(none), in which case any inferred bounds works for e2.
• the inferred bounds of e2 is bounds(any).

Testing:

• Added two new test cases. In one case, the bounds has syntactically identical. In another case, they are not syntactically identical because of the way that 'count' expands, so we produce a warning. When we extend the bounds subsumption check to understand facts about variables being equal, the second test case should no longer produce a warning