SAL. Contract programming from Microsoft or how to help a static analyzer

Source code annotation language (SAL).
In my opinion this topic is undeservedly overlooked: not a single mention has been made in runet.
No static analyzer can help you yourself.

The article is addressed to programmers who do not trust themselves and others.
People using a static analyzer or going to use.

Prehistory

.
POS terminal. 50 thousand lines. 10 years of history. Pure 'C', not knowing modern compilers. And I'm all in white.
Before you enter something you need to protect the rear:
1. Clearing alerts as far as possible.
2. Code analysis by static analyzers (MSVC2010, PVS-Studio, MSVC2013).

This has benefited, but the possibilities of static analyzers are limited, alas.
A simple wrapper over memcpy negates the attempts of the analyzers, and there is no reason to say about unique non-understandings of how many receiving-sending functions.
I need static GUARANTEES (you can dream it) of security code.
')
And then I wondered if it was possible to use macros from the standard Microsoft library.

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

It turned out possible and even necessary.

What for

Source code annotation language (SAL) allows you to specify to the analyzer the valid values ​​of the input-output parameters. The analyzer will then notify you of potential security breaches.

The simplest example contains 2 errors and a cure:

 //   void func (_Out_writes_z_(9) char * str) { strcpy(str, "20141201XXXXXX"); } void main() { char str[5]; //   func (str); } 

Using

Use is very trite.
Microsoft Help contains comprehensive information on this issue: msdn.microsoft.com/ru-ru/library/hh916382.aspx
#include <sal.h>
contains a brief guide to use.

Very briefly, macros:

1. _In_ link to input parameter
2. _Out_ link to output parameter
3. _In_z_ string ending in zero
4. _In_reads_ (s) array of elements
5. _Out_writes_z_ (s) array of size “s” for a string ending in zero

And so on.

Minuses

• Microsoft specificity.
• There are 2 versions of the language
• Intellisense QtCreator does not accept macros in function declarations
• Ads are becoming sophisticated

Another tool to fight.