Index: kernel/arch/abs32le/include/interrupt.h
===================================================================
--- kernel/arch/abs32le/include/interrupt.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ kernel/arch/abs32le/include/interrupt.h	(revision fc81981cb868cb75a16a2c5601de08457995187c)
@@ -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 fc81981cb868cb75a16a2c5601de08457995187c)
@@ -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];
Index: kernel/generic/include/verify.h
===================================================================
--- kernel/generic/include/verify.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ kernel/generic/include/verify.h	(revision fc81981cb868cb75a16a2c5601de08457995187c)
@@ -40,19 +40,31 @@
 
 #define ATOMIC         __specification_attr("atomic_inline", "")
-#define READS(...)     __specification(reads(__VA_ARGS__))
-#define WRITES(...)    __specification(writes(__VA_ARGS__))
+
+#define READS(ptr)     __specification(reads(ptr))
+#define WRITES(ptr)    __specification(writes(ptr))
 #define REQUIRES(...)  __specification(requires __VA_ARGS__)
 
-#define REQUIRES_EXTENT_MUTABLE(...) \
-	REQUIRES(\extent_mutable(__VA_ARGS__))
+#define EXTENT(ptr)              \extent(ptr)
+#define ARRAY_RANGE(ptr, nmemb)  \array_range(ptr, nmemb)
+
+#define REQUIRES_EXTENT_MUTABLE(ptr) \
+	REQUIRES(\extent_mutable(ptr))
+
+#define REQUIRES_ARRAY_MUTABLE(ptr, nmemb) \
+	REQUIRES(\mutable_array(ptr, nmemb))
 
 #else /* CONFIG_VERIFY_VCC */
 
 #define ATOMIC
-#define READS(...)
-#define WRITES(...)
+
+#define READS(ptr)
+#define WRITES(ptr)
 #define REQUIRES(...)
 
-#define REQUIRES_EXTENT_MUTABLE(...)
+#define EXTENT(ptr)
+#define ARRAY_RANGE(ptr, nmemb)
+
+#define REQUIRES_EXTENT_MUTABLE(ptr)
+#define REQUIRES_ARRAY_MUTABLE(ptr, nmemb)
 
 #endif /* CONFIG_VERIFY_VCC */
Index: tools/checkers/vcc.h
===================================================================
--- tools/checkers/vcc.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ tools/checkers/vcc.h	(revision fc81981cb868cb75a16a2c5601de08457995187c)
@@ -54,4 +54,5 @@
 __specification(typedef void * \object;)
 __specification(typedef __int64 \integer;)
+__specification(typedef unsigned __int64 \size_t;)
 
 __specification_type(objset)
@@ -66,4 +67,7 @@
 
 __specification(bool \extent_mutable(\object);)
+__specification(\objset \extent(\object);)
+__specification(\objset \array_range(\object, \size_t);)
+__specification(bool \mutable_array(\object, \size_t);)
 
 #endif