How does the _Pre_defensive_ annotation work?

So I am reasonably conversant with using Microsoft Source Annotation Language (the VS 2012-2013 flavor) to describe function contracts with pointers.

One thing I'm curious about, though, is that I expected to get a different result with _In_ _Pre_defensive_ than without it for cases where the annotated callee isn't checking the pointer first. [Many of our legacy functions expect valid input for these parameters, but the policy is to double-check.] Is there a static analysis error to describe a function marked as defensive not defending itself?

From the docs,

If a function appears at a trust boundary, we recommend that you use the _Pre_defensive_ annotation. The "defensive" modifier modifies certain annotations to indicate that, at the point of call, the interface should be checked strictly, but in the implementation body it should assume that incorrect parameters might be passed. In that case, In _Pre_defensive_ is preferred at a trust boundary to indicate that although a caller will get an error if it attempts to pass NULL, the function body will be analyzed as if the parameter might be NULL, and any attempts to de-reference the pointer without first checking it for NULL will be flagged.

Here's a little demo program for code analysis. All 4 of my functions show C6387 in the static analysis, but I was hoping to see an additional indication that my 'defensive' function wasn't actually checking the input as in fun0(). Is there any benefit to adding this qualifier? It really clutters up the declaration, so if it isn't helping, it's hard to justify putting it there.

// SAL2013.cpp : Defines the entry point for the console application.

#include "stdafx.h"

// pre-defensive annotation, but no check
void fun0(_In_ _Pre_defensive_ int* pInt)
{
    auto oops = *pInt;
}

// not defensive, no check
void fun1(_In_ int* pInt)
{
    auto oops = *pInt;
}

// defensive check, but not annotated defensively
void fun2(_In_ int* pInt)
{
    if (pInt != nullptr)
    {
        auto oops = *pInt;
    }
}

// defensive, with annotation
void fun3(_In_ _Pre_defensive_ int* pInt)
{
    if (pInt != nullptr)
    {
        auto oops = *pInt;
    }
}

int _tmain(int argc, _TCHAR* argv[])
{
    int* p = nullptr;
    fun0(p); // C6387 Invalid Parameter Value
    fun1(p); // C6387 Invalid Parameter Value
    fun2(p); // C6387 Invalid Parameter Value
    fun3(p); // C6387 Invalid Parameter Value

    return 0;
}

Bonus question: I see in sal.h there's an _In_defensive_(annotes) annotation as well, but I don't understand how to use it.

Thanks.

AFAICT there currently is no (public) difference when adding the _defensive_ annotations. However, Microsoft has additional & expanded analyzers which they use internally. These might make use of the annotations, and also may get released to the public in the future.

So it is a tradeoff. If you think they clutter the declaration too much, there is no real harm in removing them (although note that via _Use_decl_annotations_ you only need to put the annotation in the header). On the other hand, in the future this may get used, and it also can be used as documentation on intended use.

EDIT: As for _In_defensive_(annotes), it allows you to apply the _Pre_defensive_ annotation to all annotations (given in annotes). Also, this allows you place the annotation in a different place, i.e.

_In_defensive(_Pre_satisfies_(pInt != nullptr))
void fun3(int* pInt)
{
}