- debug(" kernel loaded at 0x%08lx, end = 0x%08lx\n", load, *load_end);
+ flush_len = load_end - load;
+ if (flush_start < load)
+ flush_len += load - flush_start;
+
+ flush_cache(flush_start, ALIGN(flush_len, ARCH_DMA_MINALIGN));
+
+ debug(" kernel loaded at 0x%08lx, end = 0x%08lx\n", load, load_end);