Changeset cefb126 in mainline for tools/checkers/vcc.h

Timestamp:

2010-07-02T14:19:30Z (15 years ago)

Author:

Jakub Jermar <jakub@…>

Branches:

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

Children:

89c57b6

Parents:

fe7abd0 (diff), e3ee9b9 (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:

• tools/checkers/vcc.h (moved) (moved from uspace/lib/c/arch/amd64/include/limits.h ) (2 diffs)

tools/checkers/vcc.h

@@ -1 +1 @@
 /*
- * Copyright (c) 2006 Josef Cejka
+ * Copyright (c) 2010 Martin Decky
  * All rights reserved.
  *
@@ -27 +27 @@
  */
 
-/** @addtogroup libcamd64
- * @{
- */
 /** @file
+ *
+ * VCC specifications tight to the HelenOS-specific annotations.
+ *
  */
 
-#ifndef LIBC_amd64_LIMITS_H_
-#define LIBC_amd64_LIMITS_H_
+#ifndef HELENOS_VCC_H_
+#define HELENOS_VCC_H_
 
-#define LONG_MIN MIN_INT64
-#define LONG_MAX MAX_INT64
-#define ULONG_MIN MIN_UINT64
-#define ULONG_MAX MAX_UINT64
+typedef _Bool bool;
 
-#define SIZE_MIN MIN_UINT64
-#define SIZE_MAX MAX_UINT64
-#define SSIZE_MIN MIN_INT64
-#define SSIZE_MAX MAX_INT64
+#define __concat_identifiers_str(a, b)  a ## b
+#define __concat_identifiers(a, b)      __concat_identifiers_str(a, b)
+
+#define __specification_attr(key, value) \
+        __declspec(System.Diagnostics.Contracts.CodeContract.StringVccAttr, \
+            key, value)
+
+#define __specification_type(name) \
+        __specification( \
+                typedef struct __concat_identifiers(_vcc_math_type_, name) { \
+                        char _vcc_marker_for_math_type; \
+                } __concat_identifiers(\, name); \
+        )
+
+__specification(typedef void * \object;)
+__specification(typedef __int64 \integer;)
+__specification(typedef unsigned __int64 \size_t;)
+
+__specification_type(objset)
+
+__specification(struct \TypeState {
+        __specification(ghost \integer \claim_count;)
+        __specification(ghost bool \consistent;)
+        __specification(ghost \objset \owns;)
+        __specification(ghost \object \owner;)
+        __specification(ghost bool \valid;)
+};)
+
+__specification(bool \extent_mutable(\object);)
+__specification(\objset \extent(\object);)
+__specification(\objset \array_range(\object, \size_t);)
+__specification(bool \mutable_array(\object, \size_t);)
 
 #endif