How Do You Configure Pex to Respect Code Contracts?

Question

Given the following example code, how can I configure Pex to respect my Code Contracts?

    public static IEnumerable<User> Administrators(this UserGroup userGroup)
    {
        Contract.Requires(userGroup != null);
        Contract.Requires(userGroup.UserList != null);

        return userGroup.UserList.Where(ul => ul.IsAdmin == true);
    }

Current Problem: When I run Pex, it's still generating test cases which violate the specified code contracts.

FYI: Here are the 'Code Contracts' settings in my csproj file.

---

EDIT: Did something break in SP1?

Answer 1

First you need to use a typed version of Requires

use ArgumentNullException as T

Also in you project properties you need to tell code cotracts to use the standard rewriter. DO NOT click assert on failure ;)

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

then your code will throw an argumetn null exception and pex can add an attribute to your pexmethod to say that it is allowed to throw it and will create a passing test that throws the exception

you can then promote those and save the unit tests

Answer 2

It violates the contracts on purpose to verify that an exception is thrown when the contract is violated. A lot of people will compile away the Requires methods in the Release build where some would say the edge cases should still be handled. It is also possible to write a custom contract failure handler which might not throw an exception or assertion failure. If you have a custom contract failure handler that doesn't prevent further execution you might cause even larger problems to happen further down the line.

What Pex does do is write the tests that violate a contract so that it passes when an exception is thrown.

TL/DR You shouldn't worry about it.

Answer 3

I had the same problem. There are two things:

1) Check that Run-time rewriting is enabled (as John suggests)

2) Make sure that your test class is decorated with [PexClass(typeof(MyClass))]

I have written the test manually so I have forgot that PexClass attribute and the contracts were treated as regular exceptions by Pex - so they were failing.

Honza

Answer 4

I also had to turn on Contract Reference Assembly to Build (I also emitted the XML doc file so I can see the contracts in VS).

This seems to be necessary for Pex to understand the contracts.