C Semantics in K Framework

[Chucky Ellison <celliso2 AT illinois.edu>]

Hello,

I'm thinking about sending out the following question to the committee
members, so I thought I would send it out here first to work out any
kinks :)  Please feel free to respond with whatever perspective you
have.

I'm wondering if the following program is undefined:

int main(void){
    register int x;
    if (0) {
        &x;
    }
}

(n1570) 6.7.1:6 says, "A declaration of an identifier for an object
with storage-class specifier register suggests that access to the
object be as fast as possible. The extent to which such suggestions
are effective is implementation-defined."  In a footnote, it then says
"... the address of any part of an object declared with storage-class
specifier register cannot be computed, either explicitly (by use of
the unary & operator as discussed in 6.5.3.2) or implicitly (by
converting an array name to a pointer as discussed in 6.3.2.1)."

This restriction on "register" is super important, as it is used in
6.3.2.1:2 to identify another very important class of undefined
behaviors, having to do with reading uninitialized values.  It seems
to be the only text in the standard that explicitly undefines reading
uninitialized values**.  "If the lvalue [being evaluated] designates
an object of automatic storage duration that could have been declared
with the register storage class (never had its address taken), and
that object is uninitialized (not declared with an initializer and no
assignment to it has been performed prior to use), the behavior is
undefined."

So in total, we have (in a footnote) "the address ... cannot be
computed" and (in the body) "never had its address taken" used to
describe the restriction on the register storage class.  Are these
static or dynamic concepts?  Neither of these sections are
"constraint" sections, so the restriction is not automatically static
and needs not be checked by an implementation.  Assuming a dynamic
interpretation, the words "never had" are particularly interesting, as
they suggest (at least to me) "up until that point in the execution".
Otherwise, it should say "never has".

Any thoughts?


** Excepting the fact that uninitialized values are indeterminate, and
so can possibly be trap values depending on the type.

-Chucky