Index: kernel/arch/abs32le/include/atomic.h
===================================================================
--- kernel/arch/abs32le/include/atomic.h	(revision 09a0bd4a4ab5a70550f327984b135164b05aa58d)
+++ kernel/arch/abs32le/include/atomic.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
@@ -42,4 +42,6 @@
 
 ATOMIC static inline void atomic_inc(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count < ATOMIC_COUNT_MAX)
 {
@@ -51,4 +53,6 @@
 
 ATOMIC static inline void atomic_dec(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count > ATOMIC_COUNT_MIN)
 {
@@ -60,4 +64,6 @@
 
 ATOMIC static inline atomic_count_t atomic_postinc(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count < ATOMIC_COUNT_MAX)
 {
@@ -73,4 +79,6 @@
 
 ATOMIC static inline atomic_count_t atomic_postdec(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count > ATOMIC_COUNT_MIN)
 {
@@ -89,4 +97,6 @@
 
 ATOMIC static inline atomic_count_t test_and_set(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	/* On real hardware the retrieving of the original
@@ -99,18 +109,10 @@
 }
 
-ATOMIC static inline atomic_count_t arch_atomic_get(atomic_t *val)
-{
-	/* This function is not needed on real hardware, it just
-	   duplicates the functionality of atomic_get(). It is
-	   defined here because atomic_get() is an inline function
-	   declared in a header file which we are included in. */
-	
-	return val->count;
-}
-
 static inline void atomic_lock_arch(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	do {
-		while (arch_atomic_get(val));
+		while (val->count);
 	} while (test_and_set(val));
 }
Index: kernel/generic/include/atomic.h
===================================================================
--- kernel/generic/include/atomic.h	(revision 09a0bd4a4ab5a70550f327984b135164b05aa58d)
+++ kernel/generic/include/atomic.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
@@ -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 09a0bd4a4ab5a70550f327984b135164b05aa58d)
+++ kernel/generic/include/verify.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
@@ -39,11 +39,20 @@
 #ifdef CONFIG_VERIFY_VCC
 
-#define ATOMIC         __spec_attr("atomic_inline", "")
-#define REQUIRES(...)  __requires(__VA_ARGS__)
+#define ATOMIC         __specification_attr("atomic_inline", "")
+#define READS(...)     __specification(reads(__VA_ARGS__))
+#define WRITES(...)    __specification(writes(__VA_ARGS__))
+#define REQUIRES(...)  __specification(requires __VA_ARGS__)
+
+#define REQUIRES_EXTENT_MUTABLE(...) \
+	REQUIRES(\extent_mutable(__VA_ARGS__))
 
 #else /* CONFIG_VERIFY_VCC */
 
 #define ATOMIC
+#define READS(...)
+#define WRITES(...)
 #define REQUIRES(...)
+
+#define REQUIRES_EXTENT_MUTABLE(...)
 
 #endif /* CONFIG_VERIFY_VCC */
Index: tools/checkers/vcc.h
===================================================================
--- tools/checkers/vcc.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ tools/checkers/vcc.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
@@ -0,0 +1,72 @@
+/*
+ * Copyright (c) 2010 Martin Decky
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ *
+ * - Redistributions of source code must retain the above copyright
+ *   notice, this list of conditions and the following disclaimer.
+ * - Redistributions in binary form must reproduce the above copyright
+ *   notice, this list of conditions and the following disclaimer in the
+ *   documentation and/or other materials provided with the distribution.
+ * - The name of the author may not be used to endorse or promote products
+ *   derived from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
+ * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
+ * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
+ * IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
+ * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
+ * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
+ * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/** @file
+ *
+ * VCC specifications tight to the HelenOS-specific annotations.
+ *
+ */
+
+#ifndef HELENOS_VCC_H_
+#define HELENOS_VCC_H_
+
+typedef _Bool bool;
+
+#define __concat_identifiers_str(a, b)  a ## b
+#define __concat_identifiers(a, b)      __concat_identifiers_str(a, b)
+
+#define __specification_attr(key, value) \
+	__declspec(System.Diagnostics.Contracts.CodeContract.StringVccAttr, \
+	    key, value)
+
+#define __specification_type(name) \
+	__specification( \
+		typedef struct __concat_identifiers(_vcc_math_type_, name) { \
+			char _vcc_marker_for_math_type; \
+		} __concat_identifiers(\, name); \
+	)
+
+__specification(typedef void * \object;)
+__specification(typedef __int64 \integer;)
+
+__specification_type(objset)
+
+__specification(struct \TypeState {
+	__specification(ghost \integer \claim_count;)
+	__specification(ghost bool \consistent;)
+	__specification(ghost \objset \owns;)
+	__specification(ghost \object \owner;)
+	__specification(ghost bool \valid;)
+};)
+
+__specification(bool \extent_mutable(\object);)
+
+#endif
+
+/** @}
+ */
Index: tools/checkers/vcc.py
===================================================================
--- tools/checkers/vcc.py	(revision 09a0bd4a4ab5a70550f327984b135164b05aa58d)
+++ tools/checkers/vcc.py	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
@@ -45,4 +45,6 @@
 re_va_list = re.compile("__builtin_va_list")
 
+specification = ""
+
 def usage(prname):
 	"Print usage syntax"
@@ -57,4 +59,6 @@
 	"Preprocess source using GCC preprocessor and compatibility tweaks"
 	
+	global specification
+	
 	args = ['gcc', '-E']
 	args.extend(options.split())
@@ -69,10 +73,5 @@
 	
 	tmpf = file(tmpfname, "w")
-	
-	tmpf.write("__specification(const char * const \\declspec_atomic_inline;)\n\n");
-	
-	tmpf.write("#define __spec_attr(key, value) \\\n");
-	tmpf.write("	__declspec(System.Diagnostics.Contracts.CodeContract.StringVccAttr, \\\n");
-	tmpf.write("	    key, value)\n\n");
+	tmpf.write(specification)
 	
 	for line in preproc.splitlines():
@@ -155,5 +154,5 @@
 		# Run Vcc
 		print " -- %s --" % srcfname		
-		retval = subprocess.Popen([vcc_path, '/pointersize:32', cygpath(tmpfqname)]).wait()
+		retval = subprocess.Popen([vcc_path, '/pointersize:32', '/newsyntax', cygpath(tmpfqname)]).wait()
 		
 		if (retval != 0):
@@ -170,4 +169,6 @@
 
 def main():
+	global specification
+	
 	if (len(sys.argv) < 2):
 		usage(sys.argv[0])
@@ -192,4 +193,13 @@
 		return
 	
+	specpath = os.path.join(rootdir, "tools/checkers/vcc.h")
+	if (not os.path.isfile(specpath)):
+		print "%s not found." % config
+		return
+	
+	specfile = file(specpath, "r")
+	specification = specfile.read()
+	specfile.close()
+	
 	for job in jobs:
 		if (not vcc(vcc_path, rootdir, job)):