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 a6e1ec519..72134313e 100644
--- a/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
+++ b/include/plat/pc99/plat/32/plat_mode/machine/hardware.h
@@ -46,6 +46,11 @@ pptr_to_paddr(void* pptr)
     return (paddr_t)pptr - BASE_OFFSET;
 }
 
+/* For a 32-bit system there is no difference in how we translates
+ * physical address for the kernel symbols or anything else */
+#define paddr_to_kpptr(x) paddr_to_pptr(x)
+#define kpptr_to_paddr(x) pptr_to_paddr(x)
+
 static inline region_t CONST
 paddr_to_pptr_reg(p_region_t p_reg)
 {
diff --git a/src/arch/x86/kernel/boot_sys.c b/src/arch/x86/kernel/boot_sys.c
index 019b7121c..455db8104 100644
--- a/src/arch/x86/kernel/boot_sys.c
+++ b/src/arch/x86/kernel/boot_sys.c
@@ -194,7 +194,7 @@ try_boot_sys_node(cpu_id_t cpu_id)
             )) {
         return false;
     }
-    write_cr3(pptr_to_paddr(X86_GLOBAL_VSPACE_ROOT));
+    write_cr3(kpptr_to_paddr(X86_GLOBAL_VSPACE_ROOT));
     /* Sync up the compilers view of the world here to force the PD to actually
      * be set *right now* instead of delayed */
     asm volatile("" ::: "memory");
@@ -296,7 +296,7 @@ try_boot_sys(
           );
 
     boot_state.ki_p_reg.start = PADDR_LOAD;
-    boot_state.ki_p_reg.end = pptr_to_paddr(ki_end);
+    boot_state.ki_p_reg.end = kpptr_to_paddr(ki_end);
 
     printf("Kernel loaded to: start=0x%lx end=0x%lx size=0x%lx entry=0x%lx\n",
            boot_state.ki_p_reg.start,