http://gcc.gnu.org/bugzilla/show_bug.cgi?id=56719
--- Comment #3 from felix-gcc at fefe dot de 2013-03-25 14:41:10 UTC --- @comment 1: maybe it's me but that does not make any sense. 3fff is wrong and the correct value is 3fff? Huh? @comment 2: I extracted this code from a piece of commercial production software compiled with gcc. Not sure where you draw the line but to me that makes it relevant :-)