Constant seL4_X86_VCPUObject 

pub const seL4_X86_VCPUObject: u32 = 16777214;