CODEWITHSUNDEEP
c#code-contracts
Siegeon
Siegeon

Reputation: 610

Code contract: requires unproven source != null

After reading over some of the other responses to this type of question I am still left with the warning. In this snippet I pull a UserActivation from my database. By this point there will always be at least one UserActivation. If there is more then one something has gone all pear shaped... I followed some other instructions on how to squelch the warning regarding an unproven source but to no avail.The warning is: Warning 83 CodeContracts: requires unproven: source != null on line 161, see method below for the specific line.

This is the method 

    private static UserActivation GetUserActivation(Guid userId)
    {
        UserActivations userActivations = UserActivation.GetUserActivationsByUser(userId: userId);

        Contract.Assume(userActivations != null);

        if (userActivations.Count() > 1) // Line Number 161
            throw new Exception("More then one user action found in database");

        return userActivations[0];
    }

I am using CC version 1.4.40602.0, As requested here is the UserActivations declaration. 

public class UserActivations : BusinessListBase<UserActivation>
{
    #region Constructors
    internal UserActivations()
    {
    }

    internal UserActivations(IList<UserActivation> list)
        : base(list)
    {
    }

    internal UserActivations(IEnumerable<UserActivation> list)
        : base(list)
    {
    }

And here is the GetUserActivationByUser method

    public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid())
    {
        Contract.Requires(user != null || userId != null, "Either user or userId must have a value");
        Contract.Ensures(Contract.Result<UserActivations>() != null);

        Guid id = new Guid();
        if (user != null)
            id = user.Id;
        else
            id = userId;

        return new UserActivations(StorageManager.SelectAll(
            Criteria.And(
            Criteria.EqualTo("UserId", id),
            Criteria.EqualTo("Deleted", false))));
    }

The original code was:

Public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid())
    {
        Guid id = new Guid();
        if (user != null)
            id = user.Id;
        else
            if (userId != Guid.Empty)
                id = userId;
            else
                throw new Exception("Either user or userId must have a value");

        UserActivations uas = new UserActivations(StorageManager.SelectAll(
            Criteria.And(
            Criteria.EqualTo("UserId", id),
            Criteria.EqualTo("Deleted", false))));

        Contract.Ensures(Contract.Result<UserActivations>() != null);

        return uas;
    }

Upvotes: 2

Views: 1482

Answers (2)

Pavel Gatilov
Pavel Gatilov

Reputation: 7661

Check your build log. You are using Contract.Ensures incorrectly. You should have a warning for the incorrect usage, like this one:

warning CC1025: CodeContracts: After contract block, found use of local variable 'dataEvents' defined in contract block

Your method should be:

public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid())
{
    Contract.Ensures(Contract.Result<UserActivations>() != null);

    Guid id = new Guid();
    if (user != null)
        id = user.Id;
    else
        if (userId != Guid.Empty)
            id = userId;
        else
            throw new Exception("Either user or userId must have a value");

    UserActivations uas = new UserActivations(StorageManager.SelectAll(
        Criteria.And(
        Criteria.EqualTo("UserId", id),
        Criteria.EqualTo("Deleted", false))));

    return uas;
}

I cannot prove, but I suppose this might make the verifier mad.

In fact, if I turn on run-time checks, your code won't even compile: the ccrewrite will fail.

Upvotes: 2

phoog
phoog

Reputation: 43066

I would try using a different method, perhaps avoiding the linq Enumerable extension methods. Doesn't the UserActivations class have some method or property of its own to determine how many elements an instance holds?

In any event, you shouldn't use the Count() extension method to test whether a sequence is empty, because it will enumerate the entire sequence (if the sequence does not implement ICollection). Or, as Pavel Gatilov pointed out, if the object implements IQueryable, Count may unexpectedly execute a database query.

That's not a big deal here, where you expect to have one element, but it could be a big deal in cases where a sequence might regularly have thousands of elements. Instead, you should use the Any() extension method.

Since using Any() probably won't change things from the contract analyzer's point of view, though, you should use the UserActivations class's Count property (assuming it implements ICollection, for example).

Perhaps you can help the contract analyzer this way:

private static UserActivation GetUserActivation(Guid userId) 
{ 
    UserActivations userActivations = UserActivation.GetUserActivationsByUser(userId: userId); 

    IEnumerable<UserActivation> e = (IEnumerable<UserActivation>)userActivations;

    Contract.Assume(e != null); 

    if (e.Count() > 1) // Line Number 161 
        throw new Exception("More then one user action found in database"); 

    return userActivations[0]; 
}

A better solution, if you control the UserActivations class, would be to add Contract.Ensures to GetUserActivationsByUser to say that the method will never return null.

Upvotes: 4

Related Questions