Index: kernel/arch/arm32/include/arch/mm/page_armv4.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv4.h	(revision 36df41093d27358efd761887622e3076ed51cd14)
+++ kernel/arch/arm32/include/arch/mm/page_armv4.h	(revision d776329b69ef4b29a8601fe5affe7faa8c58b51d)
@@ -44,5 +44,5 @@
 /* Macros for querying the last-level PTE entries. */
 #define PTE_VALID_ARCH(pte) \
-	(*((uint32_t *) (pte)) != 0)
+	(((pte_t *) (pte))->l0.should_be_zero != 0 || PTE_PRESENT_ARCH(pte))
 #define PTE_PRESENT_ARCH(pte) \
 	(((pte_t *) (pte))->l0.descriptor_type != 0)
Index: kernel/arch/arm32/include/arch/mm/page_armv6.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision 36df41093d27358efd761887622e3076ed51cd14)
+++ kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision d776329b69ef4b29a8601fe5affe7faa8c58b51d)
@@ -44,5 +44,5 @@
 /* Macros for querying the last-level PTE entries. */
 #define PTE_VALID_ARCH(pte) \
-	(*((uint32_t *) (pte)) != 0)
+	(((pte_t *) (pte))->l0.should_be_zero_0 != 0 || PTE_PRESENT_ARCH(pte))
 #define PTE_PRESENT_ARCH(pte) \
 	(((pte_t *) (pte))->l0.descriptor_type != 0)