Changeset 33c4f72 in mainline for kernel/generic

Timestamp:

2010-06-25T13:38:30Z (15 years ago)

Author:

Martin Decky <martin@…>

Branches:

lfn, master, serial, ticket/834-toolchain-update, topic/msim-upgrade, topic/simplify-dev-export

Children:

fc81981

Parents:

09a0bd4a

Message:

improve annotations
move to the newest VCC syntax
use VCC specifications as a separate vcc.h header

Location:

kernel/generic/include

Files:

• atomic.h (modified) (2 diffs)
• verify.h (modified) (1 diff)

kernel/generic/include/atomic.h

@@ -41 +41 @@
 
 ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
         val->count = i;
@@ -46 +48 @@
 
 ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
         return val->count;

kernel/generic/include/verify.h

@@ -39 +39 @@
 #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 */