In your presentation you shown the 'void Print(_In_ int * p)' function that demonstrates the _In_ annotation, meaning "pointer may not be null, pointed value has to be initialized".
In your opinion, does it have sense if further development of Code Analyser leads to certain language features, so that programmers are able to define three Print functions instead of one, each optimised for specific case? The first is for the case when analyser detects that the pointer is not null, therefore the function can dereference it without concern. The second is when the pointer is definitely null; this version of Print will report a compile-time error. And the third is when analyser cannot determine the previous cases; this version will contain an 'if' that detects wrong null values and throws run-time exception.