HP_NAME_SVS_ENTER_NMI
HOTPATCH(HP_NAME_SVS_ENTER_NMI, SVS_ENTER_NMI_BYTES) ; \
.name = HP_NAME_SVS_ENTER_NMI,
x86_hotpatch(HP_NAME_SVS_ENTER_NMI, 0);