armv5_dcache_wbinv_range
.cf_dcache_wbinv_range = armv5_dcache_wbinv_range,
/*XXX*/ .cf_dcache_inv_range = armv5_dcache_wbinv_range,
.cf_dcache_wbinv_range = armv5_dcache_wbinv_range,
void armv5_dcache_wbinv_range (vaddr_t, vsize_t);