[Bug c/54149] write introduction incorrect wrt the C11 memory model

[francesco.zappa.nardelli at gmail dot com]

http://gcc.gnu.org/bugzilla/show_bug.cgi?id=54149

--- Comment #1 from Francesco Zappa Nardelli <francesco.zappa.nardelli at gmail dot com> 2012-08-23 16:34:38 UTC ---
Here is another C program that hits a similar write-introduction problem:

int g_7, g_372;

char func_10 () {
  for (; g_7 < 0; ++g_7) {
  }
  return 0;
}

void main () {
  int l_8;
lbl_914:
  (l_8 = g_7) <= func_10 ();
  if (l_8)
    if (g_372) {
    } else
      goto lbl_914;
}

The reference trace is:

*** unoptimised trace: gcc --param allow-store-data-races=0 8-min.c -o
8-min_unopt

              g_7                    0  4                Init
            g_372                    0  4                Init
              g_7                    0  4                Load
              g_7                    0  4                Load

while the optimised trace (requires -O2 or -O3 to be observable) is

*** optimised trace: gcc --param allow-store-data-races=0 -O3 8-min.c -o
8-min_opt

              g_7                    0  4                Init
            g_372                    0  4                Init
            g_372                    0  4                Load
              g_7                    0  4                Load
              g_7                    0  4               Store

[ gcc version 4.8.0 20120627 (experimental) (GCC) ]