Constant seL4_VCPUReg_TTBR1high 

pub const seL4_VCPUReg_TTBR1high: Type = 39;