> It is very much an essential feature of C that one can
> reason locally. Compilers know how to reason locally,
> because in many cases they do not see the full program.

Obviously it is impossible to reason completely locally: a call to a function as simple as

  int range(const int *a,size_t n) {return a[n-1]-a[0];}

might have defined or undefined behavior based on the size of the array into which a points (let alone more exotic possibilities like a pointing too close to the end or having the wrong type). The local reasoning applied by compilers is exactly that which (they can prove) would apply for any program containing a call to the function in question that has defined behavior. The compiler does not see the full program, but its reasoning quantifies over not only all potential executions of a program but also all programs that contain the portion under examination.

> Almost all C programs are also not strictly conforming,
> but have undefined behavior. Their practical meaning is
> inferred by reasoning about individual parts.

Well, "strictly conforming" and "undefined behavior" are not exhaustive, but maybe that's not the point.

Of course global practical meanings are inferred from local (practical) meanings, but practical meanings local and global are also inferred from known behaviors of practical implementations that are not specified by any standard. I don't think the necessity of invoking such knowledge in many cases is a reason to suppose that a standard specification must be directly analogous to it (despite the resulting difficulty in representing multiple implementation possibilities).

> A specification strategy that fundamentally relies on
> quantifying over all executations of a program to decide
> whether the whole program has defined behavior or not,
> seems not very useful to me.

I see neither how that inutility follows from a notion of local reasoning nor what available specification strategy avoids such reliance. Consider the ill-advised C program

  int main() {
    int a[2]={0};
    return a[flip()]; // flip from the previous example
  }

The possible observable behaviors of this program are that it returns 0 (having accessed a[1]) or has undefined behavior (having attempted to access a[2]). Of course, that set of observable behaviors is identical to that of a program that unconditionally exhibits undefined behavior, since C says that "this document imposes no requirements" and so "the program returns 0" does not extend the set. C lacks the explicit admonition on this subject that in C++ is [intro.abstract]/5:

  However, if any such execution contains an undefined operation, this document places no requirement on the implementation executing that program with that input (not even with regard to operations preceding the first undefined operation).

This omission seems consistent with my understanding that WG14 and WG21 have not always agreed about the permission for an implementation to optimize a program under the assumption that undefined behavior never occurs. Nonetheless, I cannot avoid the conclusion that an unspecified choice between defined and undefined behavior is undefined behavior, and therefore that the status of a program having defined behavior inevitably depends on the set of all possible executions. (All of this is continuing in the tradition of ignoring the possibility of input received mid-execution that influences whether a program exhibits undefined behavior. One thing at a time.)

Davis