Index: tools/checkers/vcc.h
===================================================================
--- tools/checkers/vcc.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ tools/checkers/vcc.h	(revision cae54046b82d245b0cf3dad7ced8e4d5d09d006e)
@@ -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