Comment by cowboylowrez

> Is the critical difference here that the array access happens outside of the "for" expression?

Precisely: this means that `d[k]` is guaranteed to execute before the check that `k < 16`. In general, if you have some access like `d[k]` where `k` is some integer and `d` is some array of size `N`, you can assume that `k < N` on all paths which are dominated by the statement containing `d[k]`. In simpler terms, the optimizer will assume that `k < N` is true on every path after the access to `d[k]` occurs.

To make this clearer, consider an equivalent, slightly-transformed version of the original code:

    int d[16];
    int SATD (void)
    {
      int satd = 0, dd, k;
      dd = d[k=0];
      do {
        satd += (dd < 0 ? -dd : dd);
        k = k + 1;
        dd=d[k]; // At this point, k must be < 16.
      } while (k < 16); // The value of `k` has not changed, thus our previous
                        // assumption that `k < 16` must still hold. Thus `k < 16`
                        // can be simplified to `true`.
      return satd;
    }

Now consider a slightly-transformed version of the correct code:

    int d[16];
    int SATD (void)
    {
    int satd = 0, k = 0;
    k = 0;
    do
    {
      satd += d[k] < 0 ? -d[k] : d[k]; // At this point, k must be < 16
      k = k + 1;
    } while (k < 16); // The value of `k` has changed -- at best, we can assert
                      // that `k < 17` since its value increased by 1 since we
                      // last assumed it was less than 16. But the assumption
                      // that `k < 16` doesn't hold, and this check cannot be
                      // simplified.
    return satd;
    }

It's important that this is understood in terms of dominance (in the graph-theoretical sense), because statements like "k < 16 can never be false because it's used in d[k] where k == 16" or "the compiler will delete checks for k < 16 if it knows that d[16] occurs" which seem equivalent to the previously-stated dominance criterion simply are not. It's not that the compiler is detecting UB, thus deleting your checks -- it's that it assumes UB never occurs in the first place.