void flush_kernel_icache_page(void *);
void flush_user_dcache_page(unsigned long);
void flush_user_icache_page(unsigned long);
+void flush_user_dcache_range(unsigned long, unsigned long);
+void flush_user_icache_range(unsigned long, unsigned long);
/* Cache flush operations */