#include <stdint.h>
+#define SEL_RPL(selector) ((selector)&0x3)
+
typedef unsigned int reg32;
typedef unsigned short reg16;
: "r"(interm));
}
+static inline void
+cpu_int(int vect)
+{
+ asm("int %0" ::"i"(vect));
+}
+
void
cpu_rdmsr(uint32_t msr_idx, uint32_t* reg_high, uint32_t* reg_low);