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

[secure-sw-dev-bot]

This issue was copied from checkedc/checkedc#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:

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

[secure-sw-dev-bot]

Comment from @dtarditi:

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