Index: gcc-4.2.4/gcc/config/arm/arm.c
===================================================================
--- gcc-4.2.4.orig/gcc/config/arm/arm.c	2013-07-10 14:42:50.000000000 +0200
+++ gcc-4.2.4/gcc/config/arm/arm.c	2013-07-10 14:47:25.000000000 +0200
@@ -9866,7 +9866,7 @@
   /* If we have already generated the return instruction
      then it is futile to generate anything else.  */
   if (use_return_insn (FALSE, sibling) && return_used_this_function)
-    return "";
+    goto done;
 
   func_type = arm_current_func_type ();
 
@@ -10203,7 +10203,7 @@
 
   /* We may have already restored PC directly from the stack.  */
   if (!really_return || saved_regs_mask & (1 << PC_REGNUM))
-    return "";
+    goto done;
 
   /* Stack adjustment for exception handler.  */
   if (current_function_calls_eh_return)
@@ -10234,6 +10234,15 @@
       break;
     }
 
+done:
+  if (arm_fpu_arch == FPUTYPE_MAVERICK)
+    {
+      /* To avoid a Maverick erratum, the two words following a branch
+       * must not be Maverick insns.  Otherwise the following .words or
+       * the first insns of the following function could provoke a bug. */
+      asm_fprintf (f, "\tnop\n\tnop\n");
+    }
+
   return "";
 }