Index: kernel/arch/arm32/include/arch/mm/page_armv4.h
===================================================================
--- kernel/arch/arm32/include/arch/mm/page_armv4.h	(revision e98f1c3ecac2f8a34dd84930fa2b4ffe371c67ac)
+++ kernel/arch/arm32/include/arch/mm/page_armv4.h	(revision 42d085927b86a7b4df96490eb9d3e6d0d6ca97eb)
@@ -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 e98f1c3ecac2f8a34dd84930fa2b4ffe371c67ac)
+++ kernel/arch/arm32/include/arch/mm/page_armv6.h	(revision 42d085927b86a7b4df96490eb9d3e6d0d6ca97eb)
@@ -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)