Contract.Requires throwing pex errors [duplicate]

Question

Possible Duplicate:
How Do You Configure Pex to Respect Code Contracts?

Currently, when I run a pex exploration, the code contracts I created in my classes are being treated as errors in the pex exploration results. I thought when you ran pex exploration using code contracts the contract failures should be treated as expected behavior. Here is the code causing the exceptions.

Test Method:

[PexMethod]
public void TestEquality(Guid userId, string username, string password, string securityQuestion, string securityAnswer)
{
    UserSecurity user = UserTools.CreateUser(Guid.NewGuid(), username, password, securityQuestion, securityAnswer);

    bool passwordResult = UserTools.VerifyInput(password, user.Password, user.PasswordSalt);
    bool securityAnswerResult = UserTools.VerifyInput(securityAnswer, user.SecurityAnswer, user.SecurityAnswerSalt);

    Assert.IsTrue(passwordResult, "Password did not correctly re-hash");
    Assert.IsTrue(securityAnswerResult, "Security Answer did not correctly re-hash");
}

Failing method call:

public static UserSecurity CreateUser(Guid userId, string username, string password, string securityQuestion, string securityAnswer)
{
    Contract.Requires(userId != Guid.Empty);
    Contract.Requires(!string.IsNullOrWhiteSpace(username));
    Contract.Requires(!string.IsNullOrWhiteSpace(password));
    Contract.Requires(!string.IsNullOrWhiteSpace(securityQuestion));
    Contract.Requires(!string.IsNullOrWhiteSpace(securityAnswer));
    Contract.Ensures(Contract.Result<UserSecurity>() != null);

    byte[] passwordSalt;
    byte[] securityAnswerSalt;

    return new UserSecurity
               {
                   UserId = userId,
                   Username = username,
                   Password = SecurityUtilities.GenerateHash(password, out passwordSalt),
                   PasswordSalt = passwordSalt,
                   SecurityQuestion = securityQuestion,
                   SecurityAnswer = SecurityUtilities.GenerateHash(securityAnswer, out securityAnswerSalt),
                   SecurityAnswerSalt = securityAnswerSalt,
               };
}

--- Description

failing test: ContractException, Precondition failed: !string.IsNullOrWhiteSpace(username)

Guid s0
   = new Guid(default(int), (short)32, (short)32, default(byte), default(byte), 
              default(byte), default(byte), default(byte), 
              default(byte), default(byte), default(byte));
this.TestEquality(s0, (string)null, (string)null, (string)null, (string)null);


[TestMethod]
[PexGeneratedBy(typeof(HashTests))]
[PexRaisedContractException]
public void TestEqualityThrowsContractException173()
{
    Guid s0
       = new Guid(default(int), (short)32, (short)32, default(byte), default(byte), 
                  default(byte), default(byte), default(byte), 
                  default(byte), default(byte), default(byte));
    this.TestEquality(s0, (string)null, (string)null, (string)null, (string)null);
}

Answer 1

My understanding, from my limited experience with Pex, is that the Contract methods define the preconditions for reaching the method they are in. So, when you say

Contract.Requires(!string.IsNullOrWhiteSpace(username));

you are saying that there should be no way that statement can be reached with a null or whitespace username parameter. Pex is basically saying that you're wrong. This is one thing Pex is really good for. It means that you have the potential for a NullReferenceException or that you are not checking for an empty/whitespace username in some call to your CreateUser method. Your task, then, is to find where. You can either fix the problem by handling the null/whitespace username in the CreateUser method, then getting rid of the Contract.Requires for it, or by ensuring that all callers of CreateUser pass a non-null, non-empty username. The better choice depends on your situation, I think, but in nearly all cases, I would handle the null/whitespace username in the CreateUser method. That way, you can handle the error gracefully in one place in your code.

Of course, you really should see which caller can pass null or whitespace, since this could indicate a user input validation issue, among other potential problems.

Answer 2

I find that if you use standard contract rewriter, untick assert on failure and let your code thron ArgumentNullException by using a typed Requires argument.

contract.Requires<ArgumentNullException>(i!=null);

when you do this the methods will throw argumentnullexceptions ... pex behaves perfectly well with them.

At compile time you still get contract checking and static checking as you would expect.

It does look like PexRaisedContractException isn't behaving with how you use it. I can't say i use that attribute though. I guess from your perspective my way is a work around ;)

EDIT: Pex should generate this test, but the test should throw the error and that should cause the test to pass. the fact this is not working suggests to me that the rewriter isn't working or that the exception being thrown is not the exception type that the attribute is looking for.