How to add code substitutions for existing/uninstrumentable classes

Question

I would like to add constraints to some unmanaged method calls and to existing classes but the documentation on how to do this isn't clear.  I can add contracts for interfaces and classes of my own design just fine, but not to classes I do not have source access to.

For example say I wanted to add a replacement for Marshal.SizeOf (not complete because I can't add ContractClassAttribute to the existing Marshal class):

[assembly: ContractReferenceAssembly]
namespace My.Additional.Contracts {

    [ContractClassFor(typeof(System.Runtime.InteropServices.Marshal))]
    internal class ContractsForMarshal {
        int SizeOf(Type t) {
            Contract.Requires(t != null);
            Contract.Ensures(Contract.Result<int>() >= 0);
            return System.Runtime.InteropServices.Marshal.SizeOf(t);
        }
    }
}

Answer 1

Do you want to do this in the context of Pex, for testing, or do you ask in general about Code Contracts (independent of Pex) how to write contracts for unmanaged code?

---

---

Nikolai Tillmann - Tell us how you use Pex

Answer 2

The general Code Contracts solution would be preferred.  It's not just contracts for unmanaged code; but also for code that managed, yet non-modifiyable.  I guess I should be asking this in the Contracts forum.

Answer 3

> I guess I should be asking this in the Contracts forum.

I think that would be a good idea.

For now, to generate test cases with Pex, your best bet currently is to use moles to detour all calls to that method, and then in the attached delegate you can write assertions on the incoming argument values, choose a value to return, and write assumption on that outgoing value.

But in any case, I think you came up with a nice idea to use code contracts to specify (stateless) the assumed/guaranteed behavior of external methods; if code contracts would allow that, Pex could leverage that to automatically mole external methods.

Thanks

---

---

Nikolai Tillmann - Tell us how you use Pex