On: Could we make C arrays memory safe? Probably not, ...

[teo_zero]

I understand what the annotation does, and your examples are crystal clear. It's TFA that leaves me unconvinced.

It starts off with this function:

  int do_indexing(int *buf, const size_t bufsize, size_t index) {
    return buf[index];
  }

Later it suggests changing just the declaration, adding a parameter annotation in this way:

  int do_indexing(int *buf,
    const size_t bufsize [[arraysize_of:buf]],
    size_t index);

It suggests that, with this function declaration and the former function body, the compiler should emit a warning:

> Similarly the compiler can diagnose that the first example can lead to a buffer overflow, because the value of index can be anything.

This clashes with my understanding of why we would use the annotation in the first place. You seem to hold the same feelings, as this is analogous to your f1(), which you agree the compiler should consider safe.

Instead TFA seems to advocate that the correct function body should be:

  int do_indexing(int *buf, const size_t bufsize, size_t index) {
    if(index < bufsize)
      return buf[index];
    return -1;
  }

even with the annotated declaration:

> Now the compiler can in fact verify that the latter example is safe. When buf is dereferenced we know that the value of index is nonnegative and less than the size of the array.