This PR currently contains only the corrections that I am confident are uncontroversial. With these corrections, the example still does not work as intended in the version of the Checked C compiler as of this writing. I get the following compile error:
spec-3.6.4.c:24:16: error: it is not possible to prove that the inferred bounds of 'ap' imply the declared bounds of 'ap' after initialization
array_ptr<int> ap : count(size) = arr;
^~ ~~~
spec-3.6.4.c:24:16: note: the declared upper bounds use the variable 'size' and there is no relational information involving 'size' and any of the expressions used by the inferred upper bounds
spec-3.6.4.c:24:16: note: (expanded) declared bounds are 'bounds(ap, ap + size)'
array_ptr<int> ap : count(size) = arr;
^~
spec-3.6.4.c:24:35: note: (expanded) inferred bounds are 'bounds(arr, arr + 10)'
array_ptr<int> ap : count(size) = arr;
^~~
I could work around it by doing the initialization as follows:
array_ptr<int> ap : count(size);
void init(void) {
ap = dynamic_bounds_cast<array_ptr<int>>(arr, count(size));
}
Shall I make this change to the example in the specification too, or do you consider this an unrelated problem that doesn't merit complicating this part of the specification? (Shall I file a separate issue for the initialization error, or is there an existing issue that covers this case?)
This issue was copied from https://github.com/microsoft/checkedc/issues/478
This PR currently contains only the corrections that I am confident are uncontroversial. With these corrections, the example still does not work as intended in the version of the Checked C compiler as of this writing. I get the following compile error:
I could work around it by doing the initialization as follows:
Shall I make this change to the example in the specification too, or do you consider this an unrelated problem that doesn't merit complicating this part of the specification? (Shall I file a separate issue for the initialization error, or is there an existing issue that covers this case?)