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

Timestamp:

2010-06-25T14:49:42Z (14 years ago)

Author:

Martin Decky <martin@…>

Branches:

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

Children:

decfbe56

Parents:

33c4f72

Message:

add and improve annotations

File:

• tools/checkers/vcc.h (modified) (2 diffs)

tools/checkers/vcc.h

@@ -54 +54 @@
 __specification(typedef void * \object;)
 __specification(typedef __int64 \integer;)
+__specification(typedef unsigned __int64 \size_t;)
 
 __specification_type(objset)
@@ -66 +67 @@
 
 __specification(bool \extent_mutable(\object);)
+__specification(\objset \extent(\object);)
+__specification(\objset \array_range(\object, \size_t);)
+__specification(bool \mutable_array(\object, \size_t);)
 
 #endif