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?

Aga

Have you tried emailing them? [email protected] – Dagley

I think this is a bug. John Nicholas' solution works, but it is still not correct behavior for PEX. The point of using code contracts with pex was that PEX automatically picked up on the code contracts and treated their failure as expected behavior or a passing test. – Overmaster

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

Inbound

+1: Many thanks!! That 'Assert on Failure' setting tripped me up big time. – Aga

yeah spent a few hours smashing face into keyboard on that one myself ;) – Inbound

I think this is a work-around rather than a solution. I think that this solution may fail to detect a real "ArgumentNullException" which might be thrown from somewhere else in the code under test. I propose an alternate solution, which does not have this problem, in my answer. – Inscription

Disagree as that piece of code shuold handle its exception also .. that would then be bubbled up contractualy. – Inbound

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.

Rance

Thanks for the information, Bryan. Just curious though - Is there a way that I can tell Pex to expect the exception and to mark that test green when it violates the contract? – Aga

Pex should mark the test green when it violates the contract automatically if the contract throws an assertion or exception. – Rance

It should, but I think the current implementation is broken. I am having an issue with it currently. #5846110 – Overmaster

@Joshua Dale: @John Nicholas solution worked for me. Please give it a shot. – Aga

That is a fix, but it is still not correct behavior. The tests should automatically pick up the code contracts and treat failures as expected behavior. – Overmaster

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

Faceharden

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.

Socorrosocotra

Answer 5

There is an attribute PexAllowedContractRequiresFailure that you can decorate your test method in order to tell Pex not to generate tests that cause a requirement to fail.

You must also enable "Perform Runtime Contract Checking" in your solution properties.

[TestClass]
public partial class MyTest
{
   [PexMethod]
   [PexAllowedContractRequiresFailure]
   public void TestMethod(int myParam)
   {
      Contract.Requires(myParam > 5);
      ...
   }
}

There is also the related PexAllowedContractRequiresFailureAtTypeUnderTestSurface which I think might be helpful if the "Requires" that you want Pex to respect are deeper in the call tree.

Inscription