Quality of Visual Studio Community code analysis with SAL annotations

I hope this question is not out of scope for SO; if it is (sorry in that case), please tell me where it belongs and I'll try to move it there.

The concept of SAL annotations for static code analysis in C/C++ seems really useful to me. Take for example the wrongly implemented wmemcpy example on MSDN: Understanding SAL:

wchar_t * wmemcpy(
   _Out_writes_all_(count) wchar_t *dest,
   _In_reads_(count) const wchar_t *src,
   size_t count)
{
   size_t i;
   for (i = 0; i <= count; i++) { // BUG: off-by-one error
      dest[i] = src[i];
   }
   return dest;
}

MSDN says that "a code analysis tool could catch the bug by analyzing this function alone", which seems great, but the problem is that when I paste this code in VS 2017 Community no warning about this pops up on code analysis, not even with all analysis warnings enabled. (Other warnings like C26481 Don't use pointer arithmetic. Use span instead (bounds.1). do.)

Another example which should produce warnings (at least according to an answer to What is the purpose of SAL (Source Annotation Language) and what is the difference between SAL 1 and 2?), but does not:

_Success_(return) bool GetASmallInt(_Out_range_(0, 10) int& an_int);

//main:
int result;
const auto ret = GetASmallInt(result);
std::cout << result;

And a case of an incorrect warning:

struct MyStruct { int *a; };

void RetrieveMyStruct(_Out_ MyStruct *result) {
    result->a = new int(42);
}

//main:
MyStruct s;
RetrieveMyStruct(&s);
 // C26486 Don't pass a pointer that may be invalid to a function. Parameter 1 's.a' in call to 'RetrieveMyStruct' may be invalid (lifetime.1).
 //  Don't pass a pointer that may be invalid to a function. The parameter in a call may be invalid (lifetime.1).

result is obviously marked with _Out_ and not _In_ or _Inout_ so this warning does not make sense in this case.

My question is: Why does Visual Studio's SAL-based code analysis seem to be quite bad; am I missing something? Is Visual Studio Professional or Enterprise maybe better in this aspect? Or is there a tool which can do this better?

And if it's really quite bad: is this a known problem and are there maybe plans to improve this type of analysis?

Related: visual studio 2013 static code analysis - how reliable is it?

Functions contracts, of which SAL annotations are a lightweight realization, make it possible to reason locally about whether a function is doing the right thing and is used wrongly or the opposite. Without them, you could only discuss the notion of bug in the context of a whole program. With them, as the documentation says, it becomes possible to say locally that a function's behavior is a bug, and you can hope that a static analysis tool will find it.

Verifying mechanically that a piece of code does not have bugs remains a difficult problem even with this help. Different techniques exist because there are various partial approaches to the problem. They all have strengths and weaknesses, and they all contain plenty of heuristics. Loops are part of what makes predicting all the behaviors of a program difficult, and implementers of these tools may choose not to hard-code patterns for the extremely simple loops, since these patterns would seldom serve in practice.

And if it's really quite bad: is this a known problem and are there maybe plans to improve this type of analysis?

Yes, researchers have worked on this topic for decades and continue both to improve the theory and to transfer theoretical ideas into practical tools. As a user, you have a choice:

• if you need your code to be free of bugs, for instance because it is intended for a safety-critical context, then you already have very heavy methodology in place based on intensive testing at each level of the V-cycle, and this sort of static analysis can already help you reach the same level of confidence with less (but some) effort. You will need more expressive contract specifications than SAL annotations for this goal. An example is ACSL for C.
• if you are not willing to make the considerable effort necessary to ensure that code is bug-free with high-confidence, you can still take advantage of this sort of static analysis, but in this case consider any bug found as a bonus. The annotations, because they have a formally defined meaning, can also be useful to assign blame even in the context of a manual code review in which no static analyzer is involved. SAL annotations were designed explicitly for this usecase.