armv6_dcache_wb_range
.cf_dcache_wb_range = armv6_dcache_wb_range,
.cf_dcache_wb_range = armv6_dcache_wb_range,
.cf_dcache_wb_range = armv6_dcache_wb_range,
void armv6_dcache_wb_range (vaddr_t, vsize_t);