SAL. Контрактное программирование от Микрософт или как помочь статическому анализатору

Язык аннотации исходного кода (SAL).
По моему это тема незаслужено обойдена вниманием: не надено ни одного упоминания в рунете.
Сам себе не поможешь никакой статический анализатор тебе не поможет.

Статья адресована программистам не доверяющим себе и окружающим.
Людям, использующим статический анализатор или собирающимся использовать.

Предистория

.
POS терминал. 50тыс. строк. 10 лет истории. Чистый 'C', не знавший современных компиляторов. И Я весь в белом.
Прежде чем во что-то вступить необходимо обезопасить тылы:
1. Зачистка предупреждений, насколько это возможно.
2. Анализ кода статическими анализаторами (MSVC2010, PVS-Studio, MSVC2013).

Это принесло пользу, но возможности статических анализаторов ограничены, УВЫ.
Простая обёртка над memcpy сводит на нет потуги анализаторов, а об уникальных непойми-чего сколько принимающих-отправляющих функций и говорить не приходится.
Мне нужны статические ГАРАНТИИ (помечтать то можно) безопасности кода.

И тогда я заинтересовался: можно ли использовать макросы из стандартной библиотеки Микрософт.

void * memcpy(
   _Out_writes_bytes_all_(count) void *dest, 
   _In_reads_bytes_(count) const void *src, 
   size_t count
);

Оказалось можно и даже нужно.

Зачем

Язык аннотации исходного кода (SAL) позволяет указать анализатору допустимые значения входных-выходных парметров. После чего анализатор уведомит о потенциальных нарушениях безопасности.

Простейший пример, содержит 2 ошибки и лекарство:

// вредоносная функция 
void func (_Out_writes_z_(9) char * str)
{
      strcpy(str, "20141201XXXXXX");
}
void main()
{
    char str[5];
   // опасное использование
    func (str);
}

Использование

Использование очень банально.
Справка Микрософт содержит исчерпывающие сведения по данному вопросу: msdn.microsoft.com/ru-ru/library/hh916382.aspx
#include <sal.h>
содержит краткое руководство по использованию.

Очень кратко, макросы:

1. _In_ ссылка на входно параметр
2. _Out_ ссылка на выходной параметр
3. _In_z_ строка заканчивающаяся нулём
4. _In_reads_(s) массив элементов
5. _Out_writes_z_(s) массив размера «s» для строки заканчивающеся нулём

И так далее.

Заголовок спойлера

void func( 
_In_ int * v1, 
_In_z_ char * s,  
_In_reads_(m_len)  char * m, 
int m_len, 
_Out_writes_z_(so), int so_len)
{
      *v1;
      strlen(s);
      m[m_len - 1];
      strncpy(so, so_len, " 234234234");
}

Минусы

• Микрософт специфика.
• Существуют 2 версии языка
• Intellisense QtCreator-а не воспринимает макросов в объявлениях функций
• Объявления становятся изощрёнными

Ёщё один инструмент борьбы.