@@ -1741,10 +1741,12 @@ // Inflate byte[] array to char[]. void byte_array_inflate(Register src, Register dst, Register len, XMMRegister tmp1, Register tmp2); + void cache_wb(Address line); + void cache_wbsync(bool isPre); }; /** * class SkipIfEqual: *