// Other annotations

// Check the return value of a function e.g. _Check_return_ ErrorCode Foo();
#define _Check_return_          _Check_return_impl_

// e.g. MyPrintF( _Printf_format_string_ const wchar_t* wzFormat, ... );
#define _Printf_format_string_ _Printf_format_string_impl_
#define _Scanf_format_string_  _Scanf_format_string_impl_
#define _Scanf_s_format_string_ _Scanf_s_format_string_impl_
#define _FormatMessage_format_string_

// <expr> indicates whether post conditions apply
#define _Success_(expr)     _Success_impl_(expr)

// annotations to express 'boundedness' of integral value parameter
#define _In_bound_          _In_bound_impl_
#define _Out_bound_         _Out_bound_impl_
#define _Ret_bound_         _Ret_bound_impl_
#define _Deref_in_bound_    _Deref_in_bound_impl_
#define _Deref_out_bound_   _Deref_out_bound_impl_
#define _Deref_inout_bound_ _Deref_in_bound_ _Deref_out_bound_
#define _Deref_ret_bound_   _Deref_ret_bound_impl_

// annotations to express upper and lower bounds of integral value parameter
#define _In_range_(lb,ub)          _In_range_impl_(lb,ub)
#define _Out_range_(lb,ub)         _Out_range_impl_(lb,ub)
#define _Ret_range_(lb,ub)         _Ret_range_impl_(lb,ub)
#define _Deref_in_range_(lb,ub)    _Deref_in_range_impl_(lb,ub)
#define _Deref_out_range_(lb,ub)   _Deref_out_range_impl_(lb,ub)
#define _Deref_ret_range_(lb,ub)   _Deref_ret_range_impl_(lb,ub)

//============================================================================
//   _Pre_\_Post_ Layer:
//============================================================================

//
// _Pre_ annotation ---
//
// describing conditions that must be met before the call of the function

// e.g. int strlen( _Pre_z_ const char* sz );
// buffer is a zero terminated string
#define _Pre_z_                          _Pre2_impl_(_$notnull,  _$zterm) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_                      _Pre2_impl_(_$maybenull,_$zterm) _Deref_pre1_impl_(_$valid)

// e.g. void FreeMemory( _Pre_bytecap_(cb) _Post_ptr_invalid_ void* pv, size_t cb );
// buffer capacity described by another parameter
#define _Pre_cap_(size)                  _Pre2_impl_(_$notnull,  _$cap(size))
#define _Pre_opt_cap_(size)              _Pre2_impl_(_$maybenull,_$cap(size))
#define _Pre_bytecap_(size)              _Pre2_impl_(_$notnull,  _$bytecap(size))
#define _Pre_opt_bytecap_(size)          _Pre2_impl_(_$maybenull,_$bytecap(size))

// buffer capacity described by a constant expression
#define _Pre_cap_c_(size)                _Pre2_impl_(_$notnull,  _$cap_c(size))
#define _Pre_opt_cap_c_(size)            _Pre2_impl_(_$maybenull,_$cap_c(size))
#define _Pre_bytecap_c_(size)            _Pre2_impl_(_$notnull,  _$bytecap_c(size))
#define _Pre_opt_bytecap_c_(size)        _Pre2_impl_(_$maybenull,_$bytecap_c(size))

// buffer capacity is described by another parameter multiplied by a constant expression
#define _Pre_cap_m_(mult,size)           _Pre2_impl_(_$notnull,  _$mult(mult,size))
#define _Pre_opt_cap_m_(mult,size)       _Pre2_impl_(_$maybenull,_$mult(mult,size))

// buffer capacity described by size of other buffer, only used by dangerous legacy APIs
// e.g. int strcpy(_Pre_cap_for_(src) char* dst, const char* src);
#define _Pre_cap_for_(param)             _Pre2_impl_(_$notnull,  _$cap_for(param))
#define _Pre_opt_cap_for_(param)         _Pre2_impl_(_$maybenull,_$cap_for(param))

// buffer capacity described by a complex condition
#define _Pre_cap_x_(size)                _Pre2_impl_(_$notnull,  _$cap_x(size))
#define _Pre_opt_cap_x_(size)            _Pre2_impl_(_$maybenull,_$cap_x(size))
#define _Pre_bytecap_x_(size)            _Pre2_impl_(_$notnull,  _$bytecap_x(size))
#define _Pre_opt_bytecap_x_(size)        _Pre2_impl_(_$maybenull,_$bytecap_x(size))

// buffer capacity described by the difference to another pointer parameter
#define _Pre_ptrdiff_cap_(ptr)           _Pre2_impl_(_$notnull,  _$cap_x(__ptrdiff(ptr)))
#define _Pre_opt_ptrdiff_cap_(ptr)       _Pre2_impl_(_$maybenull,_$cap_x(__ptrdiff(ptr)))

// e.g. void AppendStr( _Pre_z_ const char* szFrom, _Pre_z_cap_(cchTo) _Post_z_ char* szTo, size_t cchTo );
#define _Pre_z_cap_(size)                _Pre3_impl_(_$notnull,  _$zterm,_$cap(size))       _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_cap_(size)            _Pre3_impl_(_$maybenull,_$zterm,_$cap(size))       _Deref_pre1_impl_(_$valid)
#define _Pre_z_bytecap_(size)            _Pre3_impl_(_$notnull,  _$zterm,_$bytecap(size))   _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_bytecap_(size)        _Pre3_impl_(_$maybenull,_$zterm,_$bytecap(size))   _Deref_pre1_impl_(_$valid)

#define _Pre_z_cap_c_(size)              _Pre3_impl_(_$notnull,  _$zterm,_$cap_c(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_cap_c_(size)          _Pre3_impl_(_$maybenull,_$zterm,_$cap_c(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_z_bytecap_c_(size)          _Pre3_impl_(_$notnull,  _$zterm,_$bytecap_c(size)) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_bytecap_c_(size)      _Pre3_impl_(_$maybenull,_$zterm,_$bytecap_c(size)) _Deref_pre1_impl_(_$valid)

#define _Pre_z_cap_x_(size)              _Pre3_impl_(_$notnull,  _$zterm,_$cap_x(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_cap_x_(size)          _Pre3_impl_(_$maybenull,_$zterm,_$cap_x(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_z_bytecap_x_(size)          _Pre3_impl_(_$notnull,  _$zterm,_$bytecap_x(size)) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_z_bytecap_x_(size)      _Pre3_impl_(_$maybenull,_$zterm,_$bytecap_x(size)) _Deref_pre1_impl_(_$valid)

// known capacity and valid but unknown readable extent
#define _Pre_valid_cap_(size)            _Pre2_impl_(_$notnull,  _$cap(size))       _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_cap_(size)        _Pre2_impl_(_$maybenull,_$cap(size))       _Deref_pre1_impl_(_$valid)
#define _Pre_valid_bytecap_(size)        _Pre2_impl_(_$notnull,  _$bytecap(size))   _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_bytecap_(size)    _Pre2_impl_(_$maybenull,_$bytecap(size))   _Deref_pre1_impl_(_$valid)

#define _Pre_valid_cap_c_(size)          _Pre2_impl_(_$notnull,  _$cap_c(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_cap_c_(size)      _Pre2_impl_(_$maybenull,_$cap_c(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_valid_bytecap_c_(size)      _Pre2_impl_(_$notnull,  _$bytecap_c(size)) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_bytecap_c_(size)  _Pre2_impl_(_$maybenull,_$bytecap_c(size)) _Deref_pre1_impl_(_$valid)

#define _Pre_valid_cap_x_(size)          _Pre2_impl_(_$notnull,  _$cap_x(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_cap_x_(size)      _Pre2_impl_(_$maybenull,_$cap_x(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_valid_bytecap_x_(size)      _Pre2_impl_(_$notnull,  _$bytecap_x(size)) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_bytecap_x_(size)  _Pre2_impl_(_$maybenull,_$bytecap_x(size)) _Deref_pre1_impl_(_$valid)

// e.g. void AppendCharRange( _Pre_count_(cchFrom) const char* rgFrom, size_t cchFrom, _Out_z_cap_(cchTo) char* szTo, size_t cchTo );
// Valid buffer extent described by another parameter
#define _Pre_count_(size)                _Pre2_impl_(_$notnull,  _$count(size))       _Deref_pre1_impl_(_$valid)
#define _Pre_opt_count_(size)            _Pre2_impl_(_$maybenull,_$count(size))       _Deref_pre1_impl_(_$valid)
#define _Pre_bytecount_(size)            _Pre2_impl_(_$notnull,  _$bytecount(size))   _Deref_pre1_impl_(_$valid)
#define _Pre_opt_bytecount_(size)        _Pre2_impl_(_$maybenull,_$bytecount(size))   _Deref_pre1_impl_(_$valid)

// Valid buffer extent described by a constant expression
#define _Pre_count_c_(size)              _Pre2_impl_(_$notnull,  _$count_c(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_opt_count_c_(size)          _Pre2_impl_(_$maybenull,_$count_c(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_bytecount_c_(size)          _Pre2_impl_(_$notnull,  _$bytecount_c(size)) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_bytecount_c_(size)      _Pre2_impl_(_$maybenull,_$bytecount_c(size)) _Deref_pre1_impl_(_$valid)

// Valid buffer extent described by a complex expression
#define _Pre_count_x_(size)              _Pre2_impl_(_$notnull,  _$count_x(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_opt_count_x_(size)          _Pre2_impl_(_$maybenull,_$count_x(size))     _Deref_pre1_impl_(_$valid)
#define _Pre_bytecount_x_(size)          _Pre2_impl_(_$notnull,  _$bytecount_x(size)) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_bytecount_x_(size)      _Pre2_impl_(_$maybenull,_$bytecount_x(size)) _Deref_pre1_impl_(_$valid)

// Valid buffer extent described by the difference to another pointer parameter
#define _Pre_ptrdiff_count_(ptr)         _Pre2_impl_(_$notnull,  _$count_x(__ptrdiff(ptr))) _Deref_pre1_impl_(_$valid)
#define _Pre_opt_ptrdiff_count_(ptr)     _Pre2_impl_(_$maybenull,_$count_x(__ptrdiff(ptr))) _Deref_pre1_impl_(_$valid)

// valid size unknown or indicated by type (e.g.:LPSTR)
#define _Pre_valid_                      _Pre1_impl_(_$notnull)   _Deref_pre1_impl_(_$valid)
#define _Pre_opt_valid_                  _Pre1_impl_(_$maybenull) _Deref_pre1_impl_(_$valid)

#define _Pre_invalid_                    _Deref_pre1_impl_(_$notvalid)

// used with allocated but not yet initialized objects
#define _Pre_notnull_                    _Pre1_impl_(_$notnull)
#define _Pre_maybenull_                  _Pre1_impl_(_$maybenull)
#define _Pre_null_                       _Pre1_impl_(_$null)

// restrict access rights
#define _Pre_readonly_                   _Pre1_impl_(_$readaccess)
#define _Pre_writeonly_                  _Pre1_impl_(_$writeaccess)
//
// _Post_ annotations ---
//
// describing conditions that hold after the function call

// void CopyStr( _In_z_ const char* szFrom, _Pre_cap_(cch) _Post_z_ char* szFrom, size_t cchFrom );
// buffer will be a zero-terminated string after the call
#define _Post_z_                        _Post1_impl_(_$zterm) _Deref_post1_impl_(_$valid)

// char * strncpy(_Out_cap_(_Count) _Post_maybez_ char * _Dest, _In_z_ const char * _Source, _In_ size_t _Count)
// buffer maybe zero-terminated after the call
#define _Post_maybez_                   _Post1_impl_(_$maybezterm)

// e.g. SIZE_T HeapSize( _In_ HANDLE hHeap, DWORD dwFlags, _Pre_notnull_ _Post_bytecap_(return) LPCVOID lpMem );
#define _Post_cap_(size)                _Post1_impl_(_$cap(size))
#define _Post_bytecap_(size)            _Post1_impl_(_$bytecap(size))

// e.g. int strlen( _In_z_ _Post_count_(return+1) const char* sz );
#define _Post_count_(size)              _Post1_impl_(_$count(size))       _Deref_post1_impl_(_$valid)
#define _Post_bytecount_(size)          _Post1_impl_(_$bytecount(size))   _Deref_post1_impl_(_$valid)
#define _Post_count_c_(size)            _Post1_impl_(_$count_c(size))     _Deref_post1_impl_(_$valid)
#define _Post_bytecount_c_(size)        _Post1_impl_(_$bytecount_c(size)) _Deref_post1_impl_(_$valid)
#define _Post_count_x_(size)            _Post1_impl_(_$count_x(size))     _Deref_post1_impl_(_$valid)
#define _Post_bytecount_x_(size)        _Post1_impl_(_$bytecount_x(size)) _Deref_post1_impl_(_$valid)

// e.g. size_t CopyStr( _In_z_ const char* szFrom, _Pre_cap_(cch) _Post_z_count_(return+1) char* szFrom, size_t cchFrom );
#define _Post_z_count_(size)            _Post2_impl_(_$zterm,_$count(size))       _Deref_post1_impl_(_$valid)
#define _Post_z_bytecount_(size)        _Post2_impl_(_$zterm,_$bytecount(size))   _Deref_post1_impl_(_$valid)
#define _Post_z_count_c_(size)          _Post2_impl_(_$zterm,_$count_c(size))     _Deref_post1_impl_(_$valid)
#define _Post_z_bytecount_c_(size)      _Post2_impl_(_$zterm,_$bytecount_c(size)) _Deref_post1_impl_(_$valid)
#define _Post_z_count_x_(size)          _Post2_impl_(_$zterm,_$count_x(size))     _Deref_post1_impl_(_$valid)
#define _Post_z_bytecount_x_(size)      _Post2_impl_(_$zterm,_$bytecount_x(size)) _Deref_post1_impl_(_$valid)

// e.g. void free( _Post_ptr_invalid_ void* pv );
#define _Post_ptr_invalid_              _Post1_impl_(_$notvalid)

// e.g. HRESULT InitStruct( _Post_valid_ Struct* pobj );
#define _Post_valid_                    _Deref_post1_impl_(_$valid)
#define _Post_invalid_                  _Deref_post1_impl_(_$notvalid)

// e.g. void ThrowExceptionIfNull( _Post_notnull_ const void* pv );
#define _Post_notnull_                  _Post1_impl_(_$notnull)

//
// _Ret_ annotations
//
// describing conditions that hold for return values after the call

// e.g. _Ret_z_ CString::operator const wchar_t*() const throw();
#define _Ret_z_                          _Ret2_impl_(_$notnull,  _$zterm) _Deref_ret1_impl_(_$valid)
#define _Ret_opt_z_                      _Ret2_impl_(_$maybenull,_$zterm) _Deref_ret1_impl_(_$valid)

// e.g. _Ret_opt_bytecap_(cb) void* AllocateMemory( size_t cb );
// Buffer capacity is described by another parameter
#define _Ret_cap_(size)                  _Ret2_impl_(_$notnull,  _$cap(size))
#define _Ret_opt_cap_(size)              _Ret2_impl_(_$maybenull,_$cap(size))
#define _Ret_bytecap_(size)              _Ret2_impl_(_$notnull,  _$bytecap(size))
#define _Ret_opt_bytecap_(size)          _Ret2_impl_(_$maybenull,_$bytecap(size))