Is this a bug in Code Analysis? Warning suppressed by _When_ clause

[EDN Admin]

I am asking this here because the Visual Studio Code Analysis and Code Metrics forum seems to lean to managed code.
Is this a bug in Code Analysis? Id expect a Read Overrun warning on third foo2 call but the _When_ clause seems to have affected the results. I do get the warning in the third foo1 call...
<span style="color:#0000aa; font-size:small void foo1(_In_ int buf_len, _In_reads_(buf_len) const char* symbol) {}
<span style="color:#0000aa; font-size:small void foo2(_In_ int buf_len, _When_(buf_len!=0, _In_reads_(buf_len)) _When_(buf_len==0, _Pre_null_) const char* symbol) {}
<span style="color:#0000aa; font-size:small //This guarantees that 2nd param of foo1 is between 1 and buf_len inclusive which then also guarantees that buf_len is > 0.<br/>
//Also guarantees, in foo2, that symbol is null when buf_len is 0 and symbol is non-null and initialized when buf_len > 0.
<span style="color:#0000aa; font-size:small char buffer[12] = {0};<br/>
foo1(sizeof buffer, buffer);<br/>
foo1(sizeof buffer-1, buffer);<br/>
foo1(sizeof buffer+1, buffer); // receive warning C6385 Read overrun<br/>
foo2(sizeof buffer, buffer);<br/>
foo2(sizeof buffer-1, buffer);<br/>
foo2(sizeof buffer+1, buffer); // did not receive warning C6385 Read overrun!<br/>
foo2(0, nullptr);<br/>
foo2(0, buffer); // receive warning C6388 Invalid parameter value<br/>
foo2(sizeof buffer, nullptr); // receive warning C6387 Invalid parameter value<br/>


View the full article