C Semantics in K Framework

[Derek M Jones <derek AT knosof.co.uk>]

Chucky,

Happy New Year all.

> I'm wondering if the following program is undefined:
>
> int main(void){
>      register int x;
>      if (0) {
>          &x;
>      }
> }

It is a constraint violation, sentence 1088
http://c0x.coding-guidelines.com/6.5.3.2.html

> 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**.

Previously is had to be inferred from the route you outline.

>                        "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."

This wording implies that access to uninitialized bit-fields and
array elements has to use the 'old' method of deducing undefined
behavior.

> 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?

Does life have to be that complicated?  Why not just flag anything that
has not been initialized?  You could do extra checks to generate
different messages.


> ** Excepting the fact that uninitialized values are indeterminate, and
> so can possibly be trap values depending on the type.
>
> -Chucky
> _______________________________________________
> c-semantics mailing list
> c-semantics AT cs.illinois.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/c-semantics

--
Derek M. Jones                  tel: +44 (0) 1252 520 667
Knowledge Software Ltd          blog:shape-of-code.coding-guidelines.com
Source code analysis            http://www.knosof.co.uk