Constant VMCS_HOST_ES 

pub const VMCS_HOST_ES: uint32_t = 0x00000c00;