http://gcc.gnu.org/bugzilla/show_bug.cgi?id=55940
--- Comment #15 from Frank Mehnert <fm3 at os dot inf.tu-dresden.de> 2013-01-16 09:01:02 UTC --- Great, thank you Jakub! As it will take some time until the Linux distributions will update their gcc binaries to include this fix, do you have any suggestion how to work around this bug by changing the code? Omitting compiler switches on the command line will not work in our scenario as the Linux kernel Makefiles define the gcc command line parameters. And can you confirm that this bug only affects 32-bit x86 targets or does it affect 64-bit x86 targets as well?