1# CONFIG_HVM is not set
2# CONFIG_PV is not set
3# CONFIG_DEBUG is not set
4