Index: kernel/generic/include/atomic.h
===================================================================
--- kernel/generic/include/atomic.h	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/include/atomic.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -41,4 +41,6 @@
 
 ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	val->count = i;
@@ -46,4 +48,5 @@
 
 ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	return val->count;
Index: kernel/generic/include/verify.h
===================================================================
--- kernel/generic/include/verify.h	(revision 22a28a696141d62f28e48ed72d1d255ff519795c)
+++ kernel/generic/include/verify.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -39,11 +39,32 @@
 #ifdef CONFIG_VERIFY_VCC
 
-#define ATOMIC         __spec_attr("atomic_inline", "")
-#define REQUIRES(...)  __requires(__VA_ARGS__)
+#define ATOMIC         __specification_attr("atomic_inline", "")
+
+#define READS(ptr)     __specification(reads(ptr))
+#define WRITES(ptr)    __specification(writes(ptr))
+#define REQUIRES(...)  __specification(requires __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(ptr)
+#define WRITES(ptr)
 #define REQUIRES(...)
+
+#define EXTENT(ptr)
+#define ARRAY_RANGE(ptr, nmemb)
+
+#define REQUIRES_EXTENT_MUTABLE(ptr)
+#define REQUIRES_ARRAY_MUTABLE(ptr, nmemb)
 
 #endif /* CONFIG_VERIFY_VCC */