No error on assignment to global variable used in bounds of another global variable (unsound)

[mattmccutchen-cci]

An assignment to a global variable that is used in the bounds of another global variable does not produce a compile error. This can lead to a buffer overflow when the second global variable is later accessed. In the analogous situation with a local variable, a compile error is correctly reported. Example:

#pragma CHECKED_SCOPE on

#include <stdlib.h>

size_t global_len = 5;
_Array_ptr<char> global_ptr : count(global_len);

int main(void) {

  size_t local_len = 5;
  _Array_ptr<char> local_ptr : count(local_len) = 0;
  local_ptr = malloc<char>(local_len);
  //local_len = 100000000;  // Compile error, as expected
  local_len = 100000000, local_ptr = malloc<char>(local_len);  // OK

  global_ptr = malloc<char>(global_len);
  global_len = 100000000;  // Should be a compile error

  for (size_t i = 0; i < global_len; i++)
    global_ptr[i]++;  // SIGSEGV

  return 0;
}

[dtarditi]

This checking isn't implemented in the compiler. The spec requires this checking be implemented. As you point out, all the machinery is there. We just need to include global variables in the list of variables being checked.