/
some_neat_examples_from_specstrings.txt
156 lines (127 loc) · 8.64 KB
/
some_neat_examples_from_specstrings.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
/* integer related macros */
#define __allocator _SAL_L_Source_(__allocator, (), __inner_allocator)
#define __deallocate(kind) _SAL_L_Source_(__deallocate, (kind), _Pre_ __notnull __post_invalid)
#define __deallocate_opt(kind) _SAL_L_Source_(__deallocate_opt, (kind), _Pre_ __maybenull __post_invalid)
#define __field_data_source(src_sym) _SAL_L_Source_(__field_data_source, (lb,ub), __inner_data_source(#src_sym))
/* Penetration review macros */
#define __in_data_source(src_sym) _SAL_L_Source_(__in_data_source, (src_sym), _Pre_ __inner_data_source(#src_sym))
#define __out_data_source(src_sym) _SAL_L_Source_(__out_data_source, (src_sym), _Post_ __inner_data_source(#src_sym))
#define __out_validated(typ_sym) _SAL_L_Source_(__out_validated, (src_sym), __inner_out_validated(#typ_sym))
#define __this_out_data_source(src_sym) _SAL_L_Source_(__this_out_data_source, (src_sym), __inner_this_data_source(#src_sym))
#define __this_out_validated(typ_sym) _SAL_L_Source_(__this_out_validated, (src_sym), __inner_this_out_validated(#typ_sym))
#define __transfer(formal) _SAL_L_Source_(__transfer, (src_sym), _Post_ __inner_transfer(formal))
#define __rpc_entry _SAL_L_Source_(__rpc_entry, (formal), __inner_control_entrypoint(RPC))
#define __kernel_entry _SAL_L_Source_(__kernel_entry, (), __inner_control_entrypoint(UserToKernel))
#define __gdi_entry _SAL_L_Source_(__gdi_entry, (), __inner_control_entrypoint(GDI))
#define __encoded_pointer _SAL_L_Source_(__encoded_pointer, (), __inner_encoded)
#define __encoded_array _SAL_L_Source_(__encoded_array, (), __inner_encoded)
#define __field_encoded_pointer _SAL_L_Source_(__field_encoded_pointer, (), __inner_encoded)
#define __field_encoded_array _SAL_L_Source_(__field_encoded_array, (), __inner_encoded)
#if defined(_MSC_EXTENSIONS) || defined(_PREFAST_) || defined(OACR) // [
#define __type_has_adt_prop(adt,prop) _SAL_L_Source_(__type_has_adt_prop, (adt,prop), __inner_adt_prop(adt,prop))
#define __out_has_adt_prop(adt,prop) _SAL_L_Source_(__out_has_adt_prop, (adt,prop), _Post_ __inner_adt_add_prop(adt,prop))
#define __out_not_has_adt_prop(adt,prop) _SAL_L_Source_(__out_not_has_adt_prop, (adt,prop), _Post_ __inner_adt_remove_prop(adt,prop))
#define __out_transfer_adt_prop(arg) _SAL_L_Source_(__out_transfer_adt_prop, (arg), _Post_ __inner_adt_transfer_prop(arg))
#define __out_has_type_adt_props(typ) _SAL_L_Source_(__out_has_type_adt_props, (typ), _Post_ __inner_adt_type_props(typ))
/* useful PFD related macros */
#define __possibly_notnullterminated _SAL_L_Source_(__possibly_notnullterminated, (), __inner_possibly_notnullterminated)
/* Windows Internal */
#define __volatile _SAL_L_Source_(__volatile, (), __inner_volatile)
#define __nonvolatile _SAL_L_Source_(__nonvolatile, (), __inner_nonvolatile)
#else
#define __out_has_type_adt_props(typ) /* nothing */
#endif
#define __deref_volatile _SAL_L_Source_(__deref_volatile, (), __deref __volatile)
#define __deref_nonvolatile _SAL_L_Source_(__deref_nonvolatile, (), __deref __nonvolatile)
/**************************************************************************
* SAL 2 extensions for Windows-specific APIs.
***************************************************************************/
// Annotation for parameters that are not used in any way by the function.
// Unlike _Reserved_, an _Unreferenced_parameter_ pointer need not be NULL.
#ifndef _Unreferenced_parameter_
#define _Unreferenced_parameter_ _SAL2_Source_(_Unreferenced_parameter_, (), _Const_)
#endif
// Pointer parameters that are freed by the function, and thus the pointed-to
// memory should not be used after return.
#ifndef _Frees_ptr_
#define _Frees_ptr_ _SAL_L_Source_(_Frees_ptr_, (), _Pre_notnull_ _Post_ptr_invalid_ __drv_freesMem(Mem))
#endif
#ifndef _Frees_ptr_opt_
#define _Frees_ptr_opt_ _SAL_L_Source_(_Frees_ptr_opt_, (), _Pre_maybenull_ _Post_ptr_invalid_ __drv_freesMem(Mem))
#endif
// Functions which behave like realloc in that they may succeed by
// freeing one block of memory and allocating another, or may fail, in
// which case the original block is still valid, or may be used to
// free memory directly by requesting that the new block is of size
// zero. We do not say here whether the before may be null, we leave
// that to the annotation on the argument
#define _Reallocation_function_(after, before, size) \
_Success_((after) != NULL || (size) == 0) \
_At_((after), _Post_maybenull_ _Post_writable_byte_size_(size) \
_When_(((before) == NULL || (size) > 0), _Must_inspect_result_)) \
_At_((before), _Post_ptr_invalid_ __drv_freesMem(Mem))
#define _Ret_reallocated_bytes_(before, size) \
_Reallocation_function_(_Curr_, before, size)
// NLS APIs allow strings to be specified either by an element count or
// null termination. Unlike _In_reads_or_z_, this is not whichever comes
// first, but based on whether the size is negative or not.
#define _In_NLS_string_(size) _SAL_L_Source_(_In_NLS_string_, (size), _When_((size) < 0, _In_z_) \
_When_((size) >= 0, _In_reads_(size)))
// Minifilter CompletionContext parameters on the pre-operation callback
// default to NULL. For return type FLT_PREOP_SUCCESS_WITH_CALLBACK or
// FLT_PREOP_SYNCHRONIZE, it may be set to NULL or a valid pointer. For all
// other returns, it must be NULL.
#define _Flt_CompletionContext_Outptr_ \
_SAL_L_Source_(_Flt_CompletionContext_Outptr_, (), _Outptr_result_maybenull_ _Pre_valid_ \
_At_(*_Curr_, _Pre_null_ \
_When_(return != FLT_PREOP_SUCCESS_WITH_CALLBACK && return != FLT_PREOP_SYNCHRONIZE, _Post_null_)))
// Minifilter ConnectionCookie parameters on the port connect notify callback
// default to NULL. On successful return, it may be set to NULL or non-NULL,
// but it must be NULL on failure.
#define _Flt_ConnectionCookie_Outptr_ \
_SAL_L_Source_(_Flt_ConnectionCookie_Outptr_, (), _Outptr_result_maybenull_ _Pre_valid_ \
_At_(*_Curr_, _Pre_null_ _On_failure_(_Post_null_)))
//
// A common pattern is to pass an "_Inout_ PCHAR* ppBuf" of size "_Inout_ DWORD* pSize"
// to a function that writes to **pBuf, incrementing *ppBuf to point to one
// past the last written byte. Thus the length of the write is
// (*ppBuf - Old(*ppBuf)). The size of the remaining unwritten capacity
// is written to *pSize.
//
// This pattern is frequently used when progressively filling a
// large buffer in chunks
// (e.g. when reading from a network interface in a driver).
//
// It is expected that these supplementary annotations would be used inside an
// _At_, like so:
//
// _At_(*ppBuf, _Writes_and_advances_ptr_(*pBufSize))
// HRESULT WriteChunkOfData(_Inout_ PCHAR* ppBuf, _Inout_ DWORD* pBufSize);
//
#ifndef _Writes_and_advances_ptr_ // [
#define _Writes_and_advances_ptr_(size) \
_SAL2_Source_(_Writes_and_advances_ptr_, (size), _At_((void*)_Curr_, _Inout_) \
_At_(_Curr_, \
_Pre_writable_size_(size) \
_Post_writable_size_(size) \
_Post_satisfies_(_Curr_ - _Old_(_Curr_) == size)) \
_At_(_Old_(_Curr_), \
_Post_readable_size_(_Old_(size) - size)))
#endif // ]
#ifndef _Writes_bytes_and_advances_ptr_ // [
#define _Writes_bytes_and_advances_ptr_(size) \
_SAL2_Source_(_Writes_bytes_and_advances_ptr, (size), _At_((void*)_Curr_, _Inout_) \
_At_(_Curr_, \
_Pre_writable_byte_size_(size) \
_Post_writable_byte_size_(size) \
_Post_satisfies_(((char*)_Curr_) - ((void*)_Old_(_Curr_)) == size)) \
_At_(_Old_(_Curr_), \
_Post_readable_byte_size_(_Old_(size) - size)))
#endif // ]
//
// Gets the current error code (as returned by GetLastError()), and stores
// in _Curr_ as a postcondition. This is currently approximated by assuming
// that GetLastError() always returns a failed error code. This is not a
// completely accurate approximation, but reasonable.
//
#define _Post_equals_last_error_ _SAL2_Source_(_Post_equals_last_error_, (), _Post_satisfies_(_Curr_ != 0))