Description
This issue was copied from checkedc/checkedc-clang#1042
Consider the following test case:
void f(int i) {
_Array_ptr<int> a : count(i) = NULL, b : bounds(a, a + i) = NULL;
a = some_helper_function();
}
The assignment a = some_helper_function() is not invertible with respect to the variable a. However, at that point, a and b produce the same value (since they are both initialized to NULL). Therefore, the original value of a in the assignment is b. a is replaced with b in the inferred bounds of b, so the inferred bounds of b after the assignment to a are bounds(b, b + i). At that point, there is no longer any relationship between a and b, so it is impossible for the compiler to prove that the inferred bounds bounds(b, b + i) of b imply the declared bounds bounds(a, a + i).
The following diagnostics are emitted:
"error: it is impossible to prove that the inferred bounds of 'b' imply the declared bounds of 'b' after assignment"
"note: the inferred bounds use the value of the variable 'b', and there is no relation between 'b' and any of the expression used in the declared bounds of 'b'"
"note: (expanded) inferred bounds: bounds(b, b + i)"
"note: (expanded) declared bounds: bounds(a, a + i)"
This is difficult to debug, since the reason why the inferred bounds of b are bounds(b, b + i) are opaque to the user. It is not apparent why a was replaced with b in the inferred bounds. To make the error message more helpful to the user, it should say something along the lines of "after assignment to the variable 'a' which is used in the declared bounds of 'b', it is not possible to reestablish the inferred bounds of 'b'".