You may be right. I haven't gone and read the standard yet, but I also fed related programs to cbmc 4.9, a C-program verifier, using the -bounds-check flag. I

You may be right. I haven't gone and read the standard yet, but I also fed related programs to cbmc 4.9, a C-program verifier, using the -bounds-check flag. It tags x[0][3] as an out-of-bounds access, but not f = &x[0][0]; f[3]; (also (x[0]+i) is OK according to cbmc, despite what we all learned about (a+b) and a[b] being the same!) Neither variant is picked up as illegal at runtime by -fsanitize=address and gcc-4.9 or clang-3.5.