Index: kernel/arch/abs32le/include/interrupt.h
===================================================================
--- kernel/arch/abs32le/include/interrupt.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ kernel/arch/abs32le/include/interrupt.h	(revision 68667ce251475e56b598e8d4f25c20a87dc24b15)
@@ -54,4 +54,5 @@
 
 static inline int istate_from_uspace(istate_t *istate)
+    REQUIRES_EXTENT_MUTABLE(istate)
 {
 	/* On real hardware this checks whether the interrupted
@@ -62,4 +63,5 @@
 
 static inline void istate_set_retaddr(istate_t *istate, uintptr_t retaddr)
+    WRITES(&istate->ip)
 {
 	/* On real hardware this sets the instruction pointer. */
@@ -69,4 +71,5 @@
 
 static inline unative_t istate_get_pc(istate_t *istate)
+    REQUIRES_EXTENT_MUTABLE(istate)
 {
 	/* On real hardware this returns the instruction pointer. */
@@ -76,4 +79,5 @@
 
 static inline unative_t istate_get_fp(istate_t *istate)
+    REQUIRES_EXTENT_MUTABLE(istate)
 {
 	/* On real hardware this returns the frame pointer. */
Index: kernel/arch/abs32le/include/mm/page.h
===================================================================
--- kernel/arch/abs32le/include/mm/page.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ kernel/arch/abs32le/include/mm/page.h	(revision 68667ce251475e56b598e8d4f25c20a87dc24b15)
@@ -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];