Index: kernel/arch/abs32le/include/mm/page.h
===================================================================
--- kernel/arch/abs32le/include/mm/page.h	(revision 6b80696ae6a6ecbf5152b450a40baedf83e9ce6c)
+++ kernel/arch/abs32le/include/mm/page.h	(revision 2ddcc7b0c2ebbacaf67571285d726dc6b2a52966)
@@ -140,4 +140,5 @@
 
 static inline unsigned int get_pt_flags(pte_t *pt, size_t i)
+    REQUIRES_ARRAY_MUTABLE(pt, PTL0_ENTRIES_ARCH)
 {
 	pte_t *p = &pt[i];
@@ -155,4 +156,6 @@
 
 static inline void set_pt_flags(pte_t *pt, size_t i, int flags)
+    WRITES(ARRAY_RANGE(pt, PTL0_ENTRIES_ARCH))
+    REQUIRES_ARRAY_MUTABLE(pt, PTL0_ENTRIES_ARCH)
 {
 	pte_t *p = &pt[i];