http://gcc.gnu.org/bugzilla/show_bug.cgi?id=55975
--- Comment #8 from Kostya Serebryany <kcc at gcc dot gnu.org> 2013-01-16 11:54:36 UTC --- Sounds good for both. Andreas, could you please try replacing kHighMemEnd = 0x00000fffffffffffUL with kHighMemEnd = 0x00003fffffffffffUL and see if it helps?