Changeset f56e897f in mainline for kernel/generic/include

Timestamp:

2010-06-29T17:43:38Z (16 years ago)

Author:

Jakub Jermar <jakub@…>

Branches:

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

Children:

6473d41

Parents:

e4a4b44 (diff), 793cf029 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge mainlnie changes.

Location:

kernel/generic/include

Files:

• atomic.h (modified) (2 diffs)
• config.h (modified) (1 diff)
• smp/ipi.h (modified) (1 diff)
• 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/config.h

@@ -70 +70 @@
         
         uintptr_t base;
-        size_t kernel_size;           /**< Size of memory in bytes taken by kernel and stack */
+        size_t kernel_size;          /**< Size of memory in bytes taken by kernel and stack */
         
-        uintptr_t stack_base;         /**< Base adddress of initial stack */
-        size_t stack_size;            /**< Size of initial stack */
+        uintptr_t stack_base;        /**< Base adddress of initial stack */
+        size_t stack_size;           /**< Size of initial stack */
 } config_t;
 

kernel/generic/include/smp/ipi.h

@@ -43 +43 @@
 #else
 
-        #define ipi_broadcast(ipi)
+#define ipi_broadcast(ipi)
 
 #endif /* CONFIG_SMP */

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(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 */