diff --git a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
index f6bafcbc1..05a8ab692 100644
--- a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
+++ b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
@@ -19,7 +19,8 @@
 #define PADDR_LOAD  0x00100000
 #define PPTR_BASE   0xe0000000
 
-#define PPTR_USER_TOP (PPTR_BASE & (~MASK(seL4_LargePageBits)))
+/* The mask here, 0xFFC00000 represents the mask for a 4MiB page. */
+#define PPTR_USER_TOP (PPTR_BASE & (0xFFC00000))
 
 /* Calculate virtual address space reserved for TLB Bitmap. ROOT_ENTRIES
  * will be zero in the case where the bitmap is unused */
diff --git a/src/plat/pc99/linker.lds b/src/plat/pc99/linker.lds
index f3860e523..461fef069 100644
--- a/src/plat/pc99/linker.lds
+++ b/src/plat/pc99/linker.lds
@@ -16,7 +16,7 @@ ENTRY(_start)
 
 CHIPSET_BASE_PADDR = 0x00000000;
 KLOAD_PADDR = 0x00100000;
-KLOAD_VADDR  = 0xe0000000;
+KLOAD_VADDR  = kernelBase;
 
 /* WARNING: constants also defined in plat/machine/hardware.h */
 #if defined(CONFIG_ARCH_IA32)