Constant seL4_X86_VCPUBits 

pub const seL4_X86_VCPUBits: u32 = 14;