UINT64 __stdcall KeFlushCurrentTbImmediately(){
unsigned __int64 v0;
UINT64 result;
v0 = __readcr4();
if( (v0 & 0x20080) != 0 )
{
result = v0 ^ 0x80;
__writecr4(v0 ^ 0x80);
__writecr4(v0);
}
else
{
result = __readcr3();
__writecr3(result);
}
return result;
}