This project is read-only.

Contracts Injector and cccheck output

Oct 31, 2010 at 9:11 PM

Hello, I have a problem: cccheck is giving less information about the contracts verification when the assembly has his contracts extracted and re-injected. For example, given this code:

using System.Diagnostics.Contracts;

namespace cc_test
    public class C
        public int M(int n)
            Contract.Requires(n > 0);

            Contract.Ensures(Contract.Result<int>() < 0);

            return n;

If I compile it and pass it through cccheck (with the default parameters that Visual Studio uses) I get this output:

OutputLine,Validated: 0%
OutputLine,Total methods analyzed 3
OutputLine,Total time 1.248sec. 416ms/method
OutputError,ensures is false: Contract.Result() < 0,,,false,False,False,error,c:\\...\\C.cs,13,13,13,22
OutputError,location related to previous warning,,,false,False,True,error,c:\\...\\C.cs,11,13,11,58
OutputSuggestion,,Checked 1 assertion: 1 false,cc_test.dll,0,0,0,0

But if I modify the assembly (and the corresponding pdb) with a code similar to the one used in the example HelloContracts extracting the contracts and re-injecting them (without modifying them), and pass that assembly to cccheck I get this output:

OutputLine,Validated: 0%
OutputLine,Total methods analyzed 3
OutputLine,Total time 1.241sec. 413ms/method
OutputError,ensures is false,,,false,False,False,error,c:\\...\\C.cs,13,13,13,22
OutputSuggestion,,Checked 1 assertion: 1 false,cc_test.mod.dll,0,0,0,0

So, basically now I don't know which contract failed. Visual Studio is able to determine the method whose verification failed with that output, but when I have more than one Ensures I can't know which one failed.

I've been looking at the extraction and injection code trying to see if something is missing (like some Locations or OriginalSource not copied), but I haven't found anything. The modified dll and pdb differ from the originals, so I think that some metadata that cccheck needs is missing.



Dec 8, 2010 at 3:39 PM
Edited Dec 8, 2010 at 5:55 PM

Sorry for the late reply!!! Please do continue to post your questions so others can benefit, but if you don't get an answer, then just poke me!

I don't know for certain, but I'm pretty sure this is completely due to missing source context information (debugging information) that is not preserved in the roundtrip. I know that debugging code that has gone through CCI doesn't work well. That is something I'm working on fixing. I don't have an estimate for when it will be ready.

In the meantime, you can try using the "-show progress -sortwarns=false" options to give you some more feedback. Once you know the exact method, then you can use the "-show il -trace dfa" options to see detailed information about that particular method. (Use "-select n" to get output just for method n. The "-show progress" option will show you the number associated with each method.)

Dec 12, 2010 at 11:02 PM

Great! Thanks for you answer.

I'll try to get more information from the verification using the options you mention.