read_msr

// Send arbitrary command to the WinDbg engine
// Returns: the command output

string @hlpIdcsend_dbg_command[send_dbg_command](string cmd);

// Read a model specific register
// Returns: the register value. if this function fails,
//          an exception with the error code is raised
// Note: this function works only in the kernel mode

int64 read_msr(long reg_id);

// Write a model specific register
// Returns: windows error code (0-ok)
// Note: this function works only in the kernel mode

success write_msr(long reg_id, int64 value);