From ad01167a92bf5bd1258a10b56ca3ee4377c7a4ec Mon Sep 17 00:00:00 2001
From: regehr <regehr>
Date: Thu, 14 Feb 2008 22:47:57 +0000
Subject: [PATCH] more annotation work

---
 tos/lib/safe/include/annots_stage1.h          | 27 +++++++++++++++++++
 .../{deputy_annots.h => annots_stage2.h}      | 13 ++++++++-
 tos/lib/safe/include/deputy_no_annots.h       |  6 -----
 tos/lib/safe/include/nesc_annots.h            |  9 -------
 tos/lib/safe/include/nesc_no_annots.h         |  9 -------
 5 files changed, 39 insertions(+), 25 deletions(-)
 create mode 100644 tos/lib/safe/include/annots_stage1.h
 rename tos/lib/safe/include/{deputy_annots.h => annots_stage2.h} (58%)
 delete mode 100644 tos/lib/safe/include/deputy_no_annots.h
 delete mode 100644 tos/lib/safe/include/nesc_annots.h
 delete mode 100644 tos/lib/safe/include/nesc_no_annots.h

diff --git a/tos/lib/safe/include/annots_stage1.h b/tos/lib/safe/include/annots_stage1.h
new file mode 100644
index 00000000..f7ea1fb3
--- /dev/null
+++ b/tos/lib/safe/include/annots_stage1.h
@@ -0,0 +1,27 @@
+#if NESC >= 130
+
+struct @bound @deputy_scope() @macro("__DEPUTY_BOUND") { void *lo, *hi; }; 
+struct @count @deputy_scope() @macro("__DEPUTY_COUNT") { int n; }; 
+struct @single @deputy_scope() @macro("__DEPUTY_SINGLE") { }; 
+struct @nonnull @deputy_scope() @macro("__DEPUTY_NONNULL") { }; 
+
+#define COUNT(x)                               @count(x)
+#define BOUND(x,y)                             @bound(x,y)
+#define SINGLE                                 @single()
+#define NONNULL                                @nonnull()
+
+#ifdef SAFE_TINYOS
+#define TCAST(__type,__expr)                   ((__type)((void * __DEPUTY_TRUSTED __DEPUTY_COPYTYPE)(__expr)))
+#define __DEPUTY_TRUSTED                       __attribute__((trusted))
+#define __DEPUTY_COPYTYPE                      __attribute__((copytype))
+#else
+#define TCAST(__type,__expr)                   ((__type)(__expr))                
+#endif
+
+#else // NESC < 130
+
+#ifdef SAFE_TINYOS
+#error Safe TinyOS requires nesC >= 1.3.0
+#endif
+
+#endif
diff --git a/tos/lib/safe/include/deputy_annots.h b/tos/lib/safe/include/annots_stage2.h
similarity index 58%
rename from tos/lib/safe/include/deputy_annots.h
rename to tos/lib/safe/include/annots_stage2.h
index 15b6f1c3..b3270224 100644
--- a/tos/lib/safe/include/deputy_annots.h
+++ b/tos/lib/safe/include/annots_stage2.h
@@ -1,6 +1,17 @@
+#ifdef SAFE_TINYOS
+
 #define __DEPUTY_BOUND(__lo,__hi)              __attribute__((bounds((__lo),(__hi))))
 #define __DEPUTY_COUNT(__n)                    __DEPUTY_BOUND(__this, __this + (__n))
 #define __DEPUTY_SINGLE(__n)                   __DEPUTY_COUNT(1)
-
 #define __DEPUTY_NONNULL(__n)                  __attribute__((nonnull))
 #define __DEPUTY_TRUSTEDBLOCK                  __blockattribute__((trusted))
+
+#else
+
+#define __DEPUTY_BOUND(__lo,__hi)              
+#define __DEPUTY_COUNT(__n)                    
+#define __DEPUTY_SINGLE(__n)                   
+#define __DEPUTY_NONNULL(__n)                  
+#define __DEPUTY_TRUSTEDBLOCK                  
+
+#endif
diff --git a/tos/lib/safe/include/deputy_no_annots.h b/tos/lib/safe/include/deputy_no_annots.h
deleted file mode 100644
index f6ac7c25..00000000
--- a/tos/lib/safe/include/deputy_no_annots.h
+++ /dev/null
@@ -1,6 +0,0 @@
-#define __DEPUTY_BOUND(__lo,__hi)              
-#define __DEPUTY_COUNT(__n)                    
-#define __DEPUTY_SINGLE(__n)                   
-
-#define __DEPUTY_NONNULL(__n)                  
-#define __DEPUTY_TRUSTEDBLOCK                  
diff --git a/tos/lib/safe/include/nesc_annots.h b/tos/lib/safe/include/nesc_annots.h
deleted file mode 100644
index b918a541..00000000
--- a/tos/lib/safe/include/nesc_annots.h
+++ /dev/null
@@ -1,9 +0,0 @@
-struct @bound @deputy_scope() @macro("__DEPUTY_BOUND") { void *lo, *hi; }; 
-struct @count @deputy_scope() @macro("__DEPUTY_COUNT") { int n; }; 
-struct @single @deputy_scope() @macro("__DEPUTY_SINGLE") { }; 
-struct @nonnull @deputy_scope() @macro("__DEPUTY_NONNULL") { }; 
-
-#define __DEPUTY_TRUSTED                       __attribute__((trusted))
-#define __DEPUTY_COPYTYPE                      __attribute__((copytype))
-#define TC(__type,__expr)                      __DEPUTY_TRUSTED_CAST(__type,__expr)
-#define __DEPUTY_TRUSTED_CAST(__type,__expr)   ((__type)((void * __DEPUTY_TRUSTED __DEPUTY_COPYTYPE)(__expr)))
diff --git a/tos/lib/safe/include/nesc_no_annots.h b/tos/lib/safe/include/nesc_no_annots.h
deleted file mode 100644
index 42565642..00000000
--- a/tos/lib/safe/include/nesc_no_annots.h
+++ /dev/null
@@ -1,9 +0,0 @@
-struct @bound @deputy_scope() @macro("__DEPUTY_BOUND") { void *lo, *hi; }; 
-struct @count @deputy_scope() @macro("__DEPUTY_COUNT") { int n; }; 
-struct @single @deputy_scope() @macro("__DEPUTY_SINGLE") { }; 
-struct @nonnull @deputy_scope() @macro("__DEPUTY_NONNULL") { }; 
-
-#define __DEPUTY_TRUSTED                       
-#define __DEPUTY_COPYTYPE                      
-#define TC(__type,__expr)                      __DEPUTY_TRUSTED_CAST(__type,__expr)   
-#define __DEPUTY_TRUSTED_CAST(__type,__expr)   ((__type)(__expr))   
-- 
2.39.2