Static checker incorrectly suggests postcondition for method returning ValidationResult

[KAW24]

When using the DataAnnotations validation system you indicate a successful validation by returning ValidationResult.Success, e.g.

public static ValidationResult IsValueValue(string valueText, ValidationContext context)
{
    // Simple example that treats any string starting with 'a' as valid
    if (valueText.StartsWith("a"))
    {
        return ValidationResult.Success;
    }
    return new ValidationResult($"The value '{valueText}' is invalid.");
}

The static checker, with check missing public ensures and suggest necessary ensures enabled, produces the following warning:

CodeContracts: Consider adding the postcondition Contract.Ensures(Contract.Result<System.ComponentModel.DataAnnotations.ValidationResult>() != null); to provide extra-documentation to the library clients

ValidationResult.Success is simply a placeholder for null to make the code more self-documenting. This means the suggested postcondition would not be valid. I could return null instead of ValidationResult.Success or suppress the warning but I think there's value in making the static checker aware of this pattern.

[SergeyTeplyakov]

I guess, static checker is correct. From "his" point of view, the result is not null and it asks to provide this semantic information.

Usually, such kind of placeholders are structs and in this case they can't be null, unlike ValidationResult that can.

[yaakov-h]

Then why does the static checker assume that ValidationResult.Success is non-null? AFAIK it should assume everything can be null unless proven otherwise.

[KAW24]

This also confused me since ValidationResult is a reference type. Does the static checker assume that read-only reference type fields are not null? This may initially seem like a reasonable assumption but obviously some class library authors think there is merit in providing a null alias. I guess the suggested postcondition is relevant to the vast majority of cases, which is something that would be lost if the static checker treated all read-only reference fields as potentially null. On the other hand, the static checker is only suggesting the postcondition to improve documentation, so it may be an acceptable loss compared to having an incorrect postcondition.