Symbol: vr4131v1_pdcache_wbinv_range_16
sys/arch/mips/include/cache_r5k.h
48
void vr4131v1_pdcache_wbinv_range_16(register_t, vsize_t);
sys/arch/mips/mips/cache.c
581
vr4131v1_pdcache_wbinv_range_16;