/* * PDE/PTE bits. These are no different from their i386 counterparts. */