hopefully final annotation syntax

diff --git a/tos/lib/safe/include/annots_stage1.h b/tos/lib/safe/include/annots_stage1.h
index 44d24463bce2f5ca7723eba90358e9a0408d4b70..f375fb9e632cf43efd53eaf4b572a3edbec96324 100644 (file)
--- a/tos/lib/safe/include/annots_stage1.h
+++ b/tos/lib/safe/include/annots_stage1.h
@@ -1,17 +1,33 @@
 #ifndef ANNOTS_STAGE1_INCLUDED
 #define ANNOTS_STAGE1_INCLUDED
+#include <stddef.h>
 
-#if NESC >= 130 && defined(SAFE_TINYOS)
+// define away two obsolete annotations
+#define BOUND(x,y)
+#define SINGLE
+
+#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") { }; 
+struct @fat @deputy_scope() @macro("__DEPUTY_FAT") { void *lo, *hi; }; 
+struct @fat_nok @deputy_scope() @macro("__DEPUTY_FAT_NOK") { void *lo, *hi; }; 
+struct @count @deputy_scope() @macro("__DEPUTY_COUNT") { int n; }; 
+struct @count_nok @deputy_scope() @macro("__DEPUTY_COUNT_NOK") { int n; }; 
+struct @one @deputy_scope() @macro("__DEPUTY_ONE") { }; 
+struct @one_nok @deputy_scope() @macro("__DEPUTY_ONE_NOK") { };
+struct @dmemset @deputy_scope() @macro("__DEPUTY_DMEMSET") {void *p; int what; size_t sz; };
+struct @dmemcpy @deputy_scope() @macro("__DEPUTY_DMEMCPY") {void *dst; void *src; size_t sz; };
 
-#define COUNT(x)                               @count(x)
-#define BOUND(x,y)                             @bound(x,y)
-#define SINGLE                                 @single()
 #define NONNULL                                @nonnull()
+#define FAT(x,y)                               @fat(x,y)
+#define FAT_NOK(x,y)                           @fat_nok(x,y)
+#define COUNT(x)                               @count(x)
+#define COUNT_NOK(x)                           @count_nok(x)
+#define ONE                                    @one()
+#define ONE_NOK                                @one_nok()
+#define DMEMSET(x,y,z)                         @dmemset(x,y,z)
+#define DMEMCPY(x,y,z)                         @dmemcpy(x,y,z)
+#define TRUSTEDBLOCK                           @unsafe()
 
 #else // NESC < 130
 
@@ -19,15 +35,20 @@ struct @nonnull @deputy_scope() @macro("__DEPUTY_NONNULL") { };
 #error Safe TinyOS requires nesC >= 1.3.0
 #endif
 
-#define COUNT(x)                               
-#define BOUND(x,y)                             
-#define SINGLE                                 
 #define NONNULL                                
+#define FAT(x,y)                             
+#define FAT_NOK(x,y)                             
+#define COUNT(x)                               
+#define COUNT_NOK(x)                               
+#define ONE 
+#define ONE_NOK
+#define DMEMSET(x,y,z)
+#define DMEMCPY(x,y,z)
+#define TRUSTEDBLOCK
 
-#endif 
+#endif // NESC version check
 
 #ifdef SAFE_TINYOS
-
 #define TCAST(__type,__expr)                   ((__type)((void * __DEPUTY_TRUSTED __DEPUTY_COPYTYPE)(__expr)))
 #define __DEPUTY_TRUSTED                       __attribute__((trusted))
 #define __DEPUTY_COPYTYPE                      __attribute__((copytype))
@@ -35,5 +56,9 @@ struct @nonnull @deputy_scope() @macro("__DEPUTY_NONNULL") { };
 #define TCAST(__type,__expr)                   ((__type)(__expr))                
 #endif 
 
-#endif // ANNOTS_STAGE1_INCLUDED
+#ifdef SAFE_TINYOS
+void * (DMEMSET(1, 2, 3) memset)(void*, int, size_t);
+void * (DMEMCPY(1, 2, 3) memcpy)(void*, const void*, size_t);
+#endif
 
+#endif

diff --git a/tos/lib/safe/include/annots_stage2.h b/tos/lib/safe/include/annots_stage2.h
index 976bcc7682d4d91757b60414a3baa58362440570..cf7717644656268ac698f98117fc073ca31d365c 100644 (file)
--- a/tos/lib/safe/include/annots_stage2.h
+++ b/tos/lib/safe/include/annots_stage2.h
@@ -3,21 +3,30 @@
 
 #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_FAT_NOK(__lo,__hi)            __attribute__((bounds((__lo),(__hi))))
+#define __DEPUTY_FAT(__lo,__hi)                __DEPUTY_NONNULL(__n) __DEPUTY_FAT_NOK(__lo,__hi)
+#define __DEPUTY_COUNT_NOK(__n)                __DEPUTY_FAT_NOK(__this, __this + (__n))
+#define __DEPUTY_COUNT(__n)                    __DEPUTY_NONNULL(__n) __DEPUTY_COUNT_NOK(__n)
+#define __DEPUTY_ONE_NOK(__n)                  __DEPUTY_COUNT_NOK(1)
+#define __DEPUTY_ONE(__n)                      __DEPUTY_NONNULL(__n) __DEPUTY_ONE_NOK(__n)
 #define __DEPUTY_TRUSTEDBLOCK                  __blockattribute__((trusted))
+#define __DEPUTY_DMEMSET(x,y,z)                __attribute__((dmemset((x),(y),(z))))
+#define __DEPUTY_DMEMCPY(x,y,z)                __attribute__((dmemcpy((x),(y),(z))))
 
 #else 
 
-#define __DEPUTY_BOUND(__lo,__hi)              
-#define __DEPUTY_COUNT(__n)                    
-#define __DEPUTY_SINGLE(__n)                   
 #define __DEPUTY_NONNULL(__n)                  
+#define __DEPUTY_FAT_NOK(__lo,__hi)              
+#define __DEPUTY_FAT(__lo,__hi)              
+#define __DEPUTY_COUNT_NOK(__n)                    
+#define __DEPUTY_COUNT(__n)                    
+#define __DEPUTY_ONE_NOK(__n)                   
+#define __DEPUTY_ONE(__n)                   
 #define __DEPUTY_TRUSTEDBLOCK                  
+#define __DEPUTY_DMEMSET(x,y,z)
+#define __DEPUTY_DMEMCPY(x,y,z)
 
 #endif 
 
 #endif 
-