Changes in kernel/generic/include/verify.h [fc81981:09a0bd4a] in mainline

File:

• kernel/generic/include/verify.h (modified) (1 diff)

kernel/generic/include/verify.h

@@ -39 +39 @@
 #ifdef CONFIG_VERIFY_VCC
 
-#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))
+#define ATOMIC         __spec_attr("atomic_inline", "")
+#define REQUIRES(...)  __requires(__VA_ARGS__)
 
 #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 */