+#ifdef CONFIG_DEBUG_DOUBLEFAULT
+ /* Only save these if we are storing them,
+ * This happens here, since L1 gets clobbered
+ * below
+ */
+ p0.l = _saved_retx;
+ p0.h = _saved_retx;
+ p1.l = _init_saved_retx;
+ p1.h = _init_saved_retx;
+ r0 = [p0];
+ [p1] = r0;
+
+ p0.l = _saved_dcplb_fault_addr;
+ p0.h = _saved_dcplb_fault_addr;
+ p1.l = _init_saved_dcplb_fault_addr;
+ p1.h = _init_saved_dcplb_fault_addr;
+ r0 = [p0];
+ [p1] = r0;
+
+ p0.l = _saved_icplb_fault_addr;
+ p0.h = _saved_icplb_fault_addr;
+ p1.l = _init_saved_icplb_fault_addr;
+ p1.h = _init_saved_icplb_fault_addr;
+ r0 = [p0];
+ [p1] = r0;
+
+ p0.l = _saved_seqstat;
+ p0.h = _saved_seqstat;
+ p1.l = _init_saved_seqstat;
+ p1.h = _init_saved_seqstat;
+ r0 = [p0];
+ [p1] = r0;
+#endif
+