This was a fork of Checked C clang used from 2021-2024. The changes have been merged into the original Checked C clang repo, which is now at https://github.com/checkedc/checkedc-clang.
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.
This issue was copied from https://github.com/microsoft/checkedc-clang/issues/1175
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:
The invertibility functions do not recognize that
p[0]is equivalent to*p, so the computed inverse ofp[0]with respect to the RHS*p + 1isnullptr. Using semantic comparison should allow the invertibility functions to computep[0] - 1(or*p - 1) as the inverse.