HelenOS sources

__specification    40 kernel/generic/include/verify.h #define READS(ptr)     __specification(reads(ptr))
__specification    41 kernel/generic/include/verify.h #define WRITES(ptr)    __specification(writes(ptr))
__specification    42 kernel/generic/include/verify.h #define REQUIRES(...)  __specification(requires __VA_ARGS__)
__specification    48 tools/checkers/vcc.h 	__specification( \
__specification    55 tools/checkers/vcc.h __specification(typedef __int64 \integer;)
__specification    56 tools/checkers/vcc.h __specification(typedef unsigned __int64 \size_t;)
__specification    60 tools/checkers/vcc.h __specification(struct \TypeState {
__specification    61 tools/checkers/vcc.h 	__specification(ghost \integer \claim_count;)
__specification    62 tools/checkers/vcc.h 	__specification(ghost bool \consistent;)
__specification    63 tools/checkers/vcc.h 	__specification(ghost \objset \owns;)
__specification    64 tools/checkers/vcc.h 	__specification(ghost \object \owner;)
__specification    65 tools/checkers/vcc.h 	__specification(ghost bool \valid;)
__specification    68 tools/checkers/vcc.h __specification(bool \extent_mutable(\object);)
__specification    69 tools/checkers/vcc.h __specification(\objset \extent(\object);)
__specification    70 tools/checkers/vcc.h __specification(\objset \array_range(\object, \size_t);)
__specification    71 tools/checkers/vcc.h __specification(bool \mutable_array(\object, \size_t);)