ls2_sdcache_wbinv_range_index
void ls2_sdcache_wbinv_range_index(vaddr_t, vsize_t);
ls2_sdcache_wbinv_range_index;
ls2_sdcache_wbinv_range_index(0, mci->mci_sdcache_way_size);