[NotNull] in Contracts Conflict with NotNullMutator

Topics: ccisharp
Oct 20, 2010 at 7:23 PM

Hi,

There is a logic bug in the Demo sample as Microsoft.Contracts consumes the [NotNull] attributes during compilation.  By the time NotNullMutator visits the IL the attributes are gone.

Thanks,

David...

Coordinator
Oct 21, 2010 at 3:05 AM

I'm sorry: I don't understand the problem. I just compiled the Demo project in CciSharp.sln and when I look at the resulting assembly in Reflector everything looks okay to me (see inserted code blocks below). Can you please be more specific about a repro?

In particular, I see the injected postcondition in Demo.Program.NeverReturnsNull:

public static string NeverReturnsNull()
{
    string Contract.Result = null;
    __ContractsRuntime.Ensures(Contract.Result > null, null, null);
    return Contract.Result;
}

 

 

I also see the injected precondition in Demo.Program.TakesNonNullParameter:

[return: MaybeNull]
public static string TakesNonNullParameter(string s)
{
    __ContractsRuntime.Requires(s > null, null, null);
    return ((s == null) ? "bad" : null);
}

 

 

Oct 21, 2010 at 8:28 PM
Edited Oct 21, 2010 at 8:34 PM

Hi,

Turns out the logic bug was in my brain. :-) This reply is to help keep others from being confused too.

I dug into the code more and found that I misunderstood the purpose of the Demo project. I was trying to manually run ccs.exe after the build. I now realize that CciSharp.targets runs ccs.exe during the build.

Additionally I found it confusing that NotNullMutator inserted Microsoft.Contracts calls into the assembly and relied upon the contracts rewriter to create the final IL. In other words the Demo project’s Code Contracts settings determine the final IL. The example you provided was for a Debug build. I was looking at a Release build in .NET Reflector with settings that do not run the rewriter. Running Demo.exe from a Release build throws an assertion.

Luckily down under the obj folder there are copies of the Demo executable from each stage of the processing. What the C# compiler generates is in Demo.csc.exe. What ccs.exe generates is in Demo.ccs.exe. What the Microsoft.Contracts rewriter generates is in Demo.exe.

Thanks,

David…

Coordinator
Oct 21, 2010 at 9:26 PM

That's funny: I thought they were all in *my* brain!

Please feel to contribute some documentation about it! It isn't easy for us to know what things are important to explain.

Actually all CciSharp does is inject *contracts*. It operates at the "code model" level and just creates the right object model to represent the contracts. Then the CCI infrastructure persists those contracts as method calls in the output. We already have a rewriter that takes calls to the contract methods and generates runtime code to enforce them. There didn't seem to be any point to duplicating that work.