Symbol: r10k_sdcache_wbinv_range_index
sys/arch/mips/include/cache_r10k.h
82
void r10k_sdcache_wbinv_range_index(vaddr_t, vsize_t);
sys/arch/mips/mips/cache.c
817
r10k_sdcache_wbinv_range_index;