c64777b77514bdc924249d2f9900be25079b0d84vboxsync; VMM - World Switchers, PAE to PAE
dd689a9d08909a7c3670e62e8b058783e0805cbcvboxsync; Copyright (C) 2006-2012 Oracle Corporation
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; This file is part of VirtualBox Open Source Edition (OSE), as
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; available from http://www.virtualbox.org. This file is free software;
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; you can redistribute it and/or modify it under the terms of the GNU
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; General Public License (GPL) as published by the Free Software
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; Foundation, in version 2 as it comes in the "COPYING" file of the
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; VirtualBox OSE distribution. VirtualBox OSE is distributed in the
a16eb14ad7a4b5ef91ddc22d3e8e92d930f736fcvboxsync; hope that it will be useful, but WITHOUT ANY WARRANTY of any kind.
f42de7470d907345da874e1613a80c2430fdf557vboxsync;*******************************************************************************
c64777b77514bdc924249d2f9900be25079b0d84vboxsync;* Defined Constants And Macros *
f42de7470d907345da874e1613a80c2430fdf557vboxsync;*******************************************************************************
c64777b77514bdc924249d2f9900be25079b0d84vboxsync%define SWITCHER_TO_PAE 1
c64777b77514bdc924249d2f9900be25079b0d84vboxsync%undef SWITCHER_TO_32BIT
c64777b77514bdc924249d2f9900be25079b0d84vboxsync%define SWITCHER_TYPE VMMSWITCHER_AMD64_TO_PAE
c64777b77514bdc924249d2f9900be25079b0d84vboxsync%define SWITCHER_DESCRIPTION "AMD64 to/from PAE"
c64777b77514bdc924249d2f9900be25079b0d84vboxsync%define NAME_OVERLOAD(name) vmmR3SwitcherAMD64ToPAE_ %+ name
c64777b77514bdc924249d2f9900be25079b0d84vboxsync;%define SWITCHER_FIX_INTER_CR3_HC FIX_INTER_AMD64_CR3
c64777b77514bdc924249d2f9900be25079b0d84vboxsync%define SWITCHER_FIX_INTER_CR3_GC FIX_INTER_PAE_CR3
f42de7470d907345da874e1613a80c2430fdf557vboxsync;*******************************************************************************
f42de7470d907345da874e1613a80c2430fdf557vboxsync;* Header Files *
f42de7470d907345da874e1613a80c2430fdf557vboxsync;*******************************************************************************