http://gcc.gnu.org/bugzilla/show_bug.cgi?id=43350
--- Comment #4 from H.J. Lu <hjl.tools at gmail dot com> 2012-11-06 22:15:02 UTC --- There is no x32 mode in hardware. Since x32 runs in 64-bit mode and only OS limits x32 address space to 32-bit, x32 process has full access to 64-bit insns, just like 64-bit process.
