diff --git a/arch/x86/include/asm/processor.h b/arch/x86/include/asm/processor.h
index 8e97d62a..398875ce 100644
--- a/arch/x86/include/asm/processor.h
+++ b/arch/x86/include/asm/processor.h
@@ -273,7 +273,7 @@ int ipi_tlb_flush(void);
 /** @brief Flush a specific page entry in TLB
  * @param addr The (virtual) address of the page to flush
  */
-static inline void tlb_flush_one_page(uint32_t addr)
+static inline void tlb_flush_one_page(size_t addr)
 {
 	asm volatile("invlpg (%0)" : : "r"(addr) : "memory");
 #if MAX_CORES > 1
@@ -293,7 +293,7 @@ static inline void tlb_flush_one_page(uint32_t addr)
  */
 static inline void tlb_flush(void)
 {
-	uint32_t val = read_cr3();
+	size_t val = read_cr3();
 
 	if (val)
 		write_cr3(val);