Invertibility does not use semantic expression comparison

[kkjeer]

When calculating the inverse of an expression, the invertibility functions do not use semantic expression comparison. This can result in errors for cases such as:

void f(_Array_ptr<_Nt_array_ptr<char>> p : count(10)) {
  p[0] = *p + 1; // error: inferred bounds for 'p[0]' are unknown after assignment
                 // note: (expanded) declared bounds are 'bounds(p[0], p[0] + 0)'
                 // note: lost the value of the expression 'p[0]' which is used in the (expanded) inferred bounds 'bounds(*p, *p + 0)' of 'p[0]'
}

The invertibility functions do not recognize that p[0] is equivalent to *p, so the computed inverse of p[0] with respect to the RHS *p + 1 is nullptr. Using semantic comparison should allow the invertibility functions to compute p[0] - 1 (or *p - 1) as the inverse.