Compiler is unable to prove that bounds(p, p + len + 1 - 1) imply bounds(p, p + len)

[kkjeer]

Consider the following example:

void f(_Nt_array_ptr<int> p : count(i), unsigned int i) {
  if (*(p + i)) {
    ++i;
  }
}

At the beginning of the statement ++i, p has the widened bounds bounds(p, p + i + 1). The original value of i is i - 1. At the end of the statement ++i, p has the inferred bounds bounds(p, p + i - 1 + 1). The compiler currently emits a warning: "cannot prove inferred bounds for p imply declared bounds for p after increment". These bounds are in fact equivalent to bounds(p, p + i) if we perform constant folding, so the compiler should not emit a warning here.

[mattmccutchen-cci]

For the record, here's the other important example that triggers this problem (from this test case, based on the new snprintf checked declaration, discussed in item 3 of microsoft/checkedc#450 (comment)):

void iface(char * restrict s : itype(restrict _Nt_array_ptr<char>) count(n-1),
           unsigned int n _Where n > 0,
           const char * restrict src : itype(restrict _Nt_array_ptr<const char>));

void iface_test2(_Nt_array_ptr<char> p : count(len), unsigned int len) {
  iface(p, len + 1, "Hello world");
}

But the widening example is interesting too!

[kkjeer]

The snprintf issue was addressed by #1095. The original issue example involving bounds widening will be addressed by #1128.

[mattmccutchen-cci]

Should this be closed now that both #1095 and #1128 are merged?