Changeset bd48f4c in mainline for kernel/generic/include/verify.h

Timestamp:

2010-07-12T10:53:30Z (14 years ago)

Author:

Jiri Svoboda <jiri@…>

Branches:

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

Children:

bd11d3e

Parents:

c40e6ef (diff), bee2d4c (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 mainline changes.

File:

• kernel/generic/include/verify.h (moved) (moved from uspace/lib/c/arch/arm32/include/limits.h ) (2 diffs)

kernel/generic/include/verify.h

@@ -1 +1 @@
 /*
- * Copyright (c) 2007 Michal Kebrt
+ * Copyright (c) 2010 Martin Decky
  * All rights reserved.
  *
@@ -27 +27 @@
  */
 
-/** @addtogroup libcarm32
+/** @addtogroup genericverify
  * @{
  */
 /** @file
- *  @brief Limits declarations.
  */
 
-#ifndef LIBC_arm32__LIMITS_H_
-#define LIBC_arm32__LIMITS_H_
+#ifndef KERN_VERIFY_H_
+#define KERN_VERIFY_H_
 
-#define LONG_MIN MIN_INT32
-#define LONG_MAX MAX_INT32
-#define ULONG_MIN MIN_UINT32
-#define ULONG_MAX MAX_UINT32
 
-#define SIZE_MIN MIN_UINT32
-#define SIZE_MAX MAX_UINT32
-#define SSIZE_MIN MIN_INT32
-#define SSIZE_MAX MAX_INT32
+#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))
+
+#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 */
+
 
 #endif