Constant seL4_VCPUReg_TTBR0high 

pub const seL4_VCPUReg_TTBR0high: Type = 38;