This commit involves the PAE paging itself, refactoring the
vspace code to extra what is common between PAE and 32bit paging,
as well as some renaming to not call the root paging structure
a PD
The c-parser can now parse these functions, but it does it by
discarding the inline ASM block, creating a misleading and likely
malformed function body. It is better to not translate these
with a DONT_TRANSLATE comment.
This change has been made for the current verification platform
only, and should probably be extended to any other verification
targets as necessary.
