Fix mistakes in the "Variables at external scope" example in the spec.

[mattmccutchen-cci]

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?)

[dtarditi]

Hi Matt, could you create a new PR here: https://github.com/checkedc/checkedc? I have left Microsoft and would like work on Checked C to continue there.

[zouyonghao]

Hi @dtarditi , I guess it should be https://github.com/checkedc/checkedc. Is that the official checkedc repo?

[dtarditi]

Hi @zouyonghao, thanks for pointing out the broken link. Yes, it should be https://github.com/checkedc/checkedc. That is where work on Checked C continues. We originally had the longer project name of secure-sw-dev, but realized no one would remember that!

[mwhicks1]

David, while I think of it: Is it possible to forward from the longer link to this one? We reference the longer address in the most recent Checked C papers (at OOPSLA'22 and CSF'23).

[dtarditi]

I've (re)claimed the organization name secure-sw-dev for the Secure Software Development Project. Yes, we can set something up to forward to the Checked C repo.