LAPIC_LVT_CMCI
.lvt_reg = LAPIC_LVT_CMCI,
printf(" cmci: 0x%08x\n", lapic_read32(LAPIC_LVT_CMCI));
lapic_write32(LAPIC_LVT_CMCI, lvt_mode(la, APIC_LVT_CMCI,
lapic_read32(LAPIC_LVT_CMCI)));