microsoft / codecontracts

Source code for the CodeContracts tools for .NET

CodeContracts

Source code for the CodeContracts tools for .NET

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs.

The contracts take the form of pre-conditions, post-conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation. Code Contracts bring the advantages of design-by-contract programming to all .NET programming languages. We currently provide three tools:

1. Runtime Checking. Our binary rewriter modifies a program by injecting the contracts, which are checked as part of program execution. Rewritten programs improve testability: each contract acts as an oracle, giving a test run a pass/fail indication. Automatic testing tools, such as Pex, take advantage of contracts to generate more meaningful unit tests by filtering out meaningless test arguments that don't satisfy the pre-conditions.
2. Static Checking. Our static checker can decide if there are any contract violations without even running the program! It checks for implicit contracts, such as null dereferences and array bounds, as well as the explicit contracts.
3. Documentation Generation. Our documentation generator augments existing XML doc files with contract information. There are also new style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

Quick Links

• Download: https://visualstudiogallery.msdn.microsoft.com/1ec7db13-3363-46c9-851f-1ce455f66970
• FAQ: http://research.microsoft.com/en-us/projects/contracts/faq.aspx
• Forum: http://social.msdn.microsoft.com/Forums/en-US/codecontracts/threads

Building from source

For working on the project, open CodeContracts.sln and build.

To create the installer and the nuget package, just run buildCC <version>.

We use the convention:

• CC major version = 1.9.1
• CC minor version = {month}{day}.{buildInTheDay}

For instance, the 10^th build on July 16 would be run as follows:

buildCC 1.9.10716.10

codecontracts's Issues

[Milestone discussion] VS2015 support

I would like to put all bugs, issues and work items into one place to simplify our first and very important milestone - support for VS2015.

I would like to focus on this first and do the rest later. It means that we should try to focus our activities to get things done and release new version (I hope to release official version with support from @mike-barnett).

I can see following areas in this milestone:

Rewriter issues

• Support for async methods. Issues - #51, fix - #74
• Issues with async methods with Contract.Ensures(Contract.ForAll) - #49, #72, #69. Fix - #74
• Issue with iterator blocks with complex precondition for async methods and iterator blocks with preconditions mode only. Issue - #38. I'll talk to original authors of this tool to understand potential fix.

VSIX support for VS2015

• I think we need to update VSIX package or installer to be able to use CC with VS2015.

❓ @sharwell Any ideas how to do this?

CC Editor Extensions

• Editor extension does not working with VS2013/VS2015. Issue: #4, Fix: #66

❓ I don't know is it really necessary for this milestone. Because Editor Extension wasn't working for VS2013 as well, I would prefer to separate this activity from this one.

Other issues

• ILMerge. Fix: #60.
• Build process issues. Issue: #70

❓ Any ideas about this milestone would be very helpful.

Unresolvable warning

public class Base
{
    public virtual string VirtualMethod(string param)
    {
        return null;  // Base class should not do anything here...
    }
}

public class Derived : Base
{
    public override string VirtualMethod(string param)
    {
        return "Test";
    }
}

This will generate a warning on the base class:

CodeContracts: Consider adding the postcondition Contract.Ensures(Contract.Result<System.String>() == null); to provide extra-documentation to the library clients

However if we add this, all derived classes must return null, too!

MSBuild 12.0 Microsoft.CodeContracts.targets imports wrong ContractAnalysis.targets

The MSBuild v12.0 version of Microsoft.CodeContracts.targets imports $(CodeContractsInstallDir)MsBuild\v4.0\Microsoft.CodeContractAnalysis.targets. This is a relatively minor issue, but causes some problems if you're trying to add the minimum requirements for Code Contracts into your source enlistment to support builds without the extension.

The problem is on line 638 with the definition of the CodeContractAnalysisTargets property. This line is fine in the MSBuild 3.5 and 4.0 versions of the file.

The best way to resolve this would be to set the property to $(MSBuildThisFileDirectory)Microsoft.CodeContractAnalysis.targets, which would prevent the need for the version number in any of the files (4.0 and up - 3.5 doesn't support MSBuildThisFile).

Most of the content could be consolidated to avoid the need for duplicating the file with each version, but this minor change would avoid at least one problem.

Can't run Foxtrot unit tests

Maybe I'm doing something wrong, but I can't run any tests from Foxtroct/UnitTests project (VS2013, tried both - VS Test Runner and R#).

All of them are failing with an error: "Can't find the TestResults directory!!!" at RewrittenContractTests.cs:89.

AssemblyInitialize method should not use Directory.CurrentDirectory but should use context property of type TestContext to grab all the required information about TestResults folders etc.

Code Contracts Abbreviators do not work if placed in a separate assembly.

We have moved frequent and common requirements to a separate assembly.
Contract.Requires<ArgumentNullException>(...) became just Requires.NotNull(...). so we have fewer typing in many places. Bu then we discovered that ccrewriter does not do its job. Abbreviators are simply ignored if they are called from another assembly.

Confusing warning about non-existing code chain

    private static int DetermineStartupMode(IEnumerable<string> args)
    {
        Contract.Requires(args != null);

        var arg = args.FirstOrDefault();

        if (arg != null)
        {
            switch (arg.ToLower().Trim())
            {
                case "a":
                    break;

                case "b":
                    return 1;

                case "c":
                    return 2;
            }
        }

        return 0;
    }

This code will generate the warning:

The Boolean condition ((string)System.Linq.Enumerable.FirstOrDefault(args)).ToLower().Trim() != null always evaluates to a constant value.

Wrong warning for static events

public class Test5
{
    public static event EventHandler SomeEvent;

    public static void RaiseTheEvent(object sender)
    {
        var eventHandler = SomeEvent;
        if (eventHandler != null)
        {
            eventHandler(sender, EventArgs.Empty);
        }
    }
}

Here we get this warning:
The Boolean condition eventHandler != null always evaluates to a constant value. If it (or its negation) appear in the source code....

If no event handler is attached to SomeEvent, it is null.

Future plans for Code Contracts

This issue is meant to provide a single place where we can keep people notified about the status of the Code Contracts project. We (Microsoft) now have some resources and will do the work (in conjunction with the community of course) to update the sources so the tools will work in VS2015. After that, we are looking to transition the repo outside of the Microsoft organization in GitHub and turn ownership over to any community members that are interested.

As far as we are aware, the current work items are:

1. Updating the rewriter to understand the new Roslyn code-generation patterns for iterators/async.
2. Updating the Visual Studio integration so that the Code Contracts pane appears in the project properties window.
3. Fixing some other missing files, etc.

Separately, there is a Roslyn discussion (dotnet/roslyn#119) about adding contracts to a future version of C#.

Centralise/Decentralise SQL Database for caching?

We are planning on implementing code contracts in a very mature product. We have already retrofitted a few years ago to our newer products and have had good success.

We intend to move contract checking outside of the build process and into our automated test framework. We run about 220 test clients each hour through about 1/2 million tests. These clients would end up running an assembly each until completion of the test run. It is possible that we may run contract testing on a daily basis if load is too great to perform on each checkin (we merge about 200 checkins daily, to create about 30 discrete test runs daily).

Do you have any advice as to whether using a centralised database would be ok for this sort of scale?
I assume we may need it to be centralised to have access to contracts from earlier assemblies in the build order?
Also, I assume we would need to stagger contract evaluation so that earlier assemblies in the build order are completed before we start later assemblies? We have a parallelised build process that does this already and could be modified to provide assemblies in the correct order.

Pull requests policies

Hello everyone.

@mike-barnett added me as an owner to this repo and I'm going to start working on pull requests and other stuff.

My team in Microsoft is using Code Contracts library super extensively and I'm going to work on this stuff in near future to get them working with VS14, fix some other bugs, review and merge pull requests etc.

I would like to be as useful as possible and I need some help from you guys. Can you help me to prioritize and review existing pull requests? I would like to see some comments here with a list of most critical pull requests that's are ready to merge and at least one "Reviewed, looks good for me" for each pull requests. (I'll review them myself and for all critical ones I would get Mike's feedback as well).

I'm a big fan of Code Contracts and I personally don't want them to die. So I would do my best to keep the source up-to-date and merge pull requests as soon as I can.

Contract assembly for Microsoft.VisualBasic.dll should define "Empty" _MYTYPE.

Using C# compiler from VS2013 produces no "My" namespace in Microsoft.VisualBasic.Contracts.dll even if _MYTYPE is set to "Windows". This behavior changed in Roslyn and in order to disable My namespace in output assembly _MYTYPE shall be set to "Empty". Setting it to "Empty" in Microsoft.VisualBasic10.vbproj file will fix compilation for VS2015 and at the same time will not change compilation results for VS2013.

Remove -nologo from msbuild task.

Currently, nologo is enabled by default when building a Code Contract enabled project from Visual Studio or MSBuild. It does not appear there is any way to disable this behavior.

As it stands now, troubleshooting code contract discrepancies between a remote build server and a local developer environment is challenging because there is no way to easily find out what version of Code Contracts is being executed on the build server or the local machine. Locally, you can check the project properties page to get the version (though this may not be what is actually executed). On a remote build server that you don't have access too, there is no way to identify the version of Code Contracts that I can find.

I believe the problem is here:
https://github.com/Microsoft/CodeContracts/blob/180c3ae426fae1c31105fc672eeba57c91f76ed0/Microsoft.Research/ManagedContract.Setup/MSBuild/v3.5/Microsoft.CodeContractAnalysis.targets#L207

But I really don't know much about the msbuild tasks in Code Contracts or how they are executed so I am not certain.

ccrefgen uses PdbFunction.ReadCustomMetadata_OLD instead of ReadCustomMetadata

PdbFunction.ReadCustomMetadata_OLD throws when there is an unknown custom metadata.
Roslyn and dynamic local variables introduce metadata types greater than 4 which causes ReadCustomMetadata to throw a PdbDebugException with the message "Unknown custom metadata item kind: {0}"

Repro at https://github.com/krk/CodeContractsRosyln

Note: ccrewrite uses the new ReadCustomMetadata, ccrefgen does not.

Installer creates a C:\VS11Root folder

Whenever I install Code Contracts, the installer creates a C:\VS11Root folder that seems to contain the Visual Studio extension. This happens with machines where VS2010 or VS2013 is installed (haven't tested VS2012).

Contract.Requires not rewritten in async methods compiled by Roslyn

There already are some open issues that deal with the rewriter missing Asserts/Assumes in async methods/iterators (notably #41), however, these are concerned with rather complex conditions in these Asserts.

This issue is about Contract.Requires with simple conditions (such as param != null) in async methods compiled by Roslyn (VS 2015).

Simple working example (class library project):

using System.Diagnostics.Contracts;
using System.Threading.Tasks;

namespace RewriterWithRoslynRepro
{
    public class Class
    {
        public async Task<int> AsyncMethod(string str)
        {
            Contract.Requires(str != null);

            await Task.Delay(100);

            return 0;
        }
    }
}

After some investigation (I am not familiar with these sources), the rewriter seems to do the following steps upon encountering an async method (i.e. a method that sets up a state machine and so on)

• it looks up the MoveNext method of the state machine that is generated by the compiler
• it simulates what MoveNext would do when it's called for the first time
• it finds an IL block "B" that possibly contains a Contract.Requires statement
• it looks up the last Contract.Requires statement that occurs after or in "B". By last, I mean highest in terms of the IL offset of the statement.

The lookup of such a block "B" succeeds for IL compiled with the native compiler but fails for Roslyn compiled IL. Upon further investigation, i found this assumption in the code.

From my experiments with Roslyn compiled code, this does not hold (any more?). The initial state is still -1. Changing this line to var initialState = isAsync ? -1 : 0; lets the rewriter find the block.

Can someone with insight into Roslyn confirm that the initial state of an async state machine is indeed -1 and not 0 ?

EDIT: According to the Roslyn sources (here and here) the initial state is indeed -1.

CCRewrite fails with NRE on async method with Ensures.ForAll with captured params

Code contracts repo has a bunch of tests for async methods. Unfortunately, some of them are broken.

For instance, tests for async6.cs to async9.cs will fail because ccrewrite.exe will return -1.

Here is a small repo for the issue:

class TestTaskContracts
{
    public async Task<List<int>> FooAsync(int limit)
    {
        Contract.Ensures(Contract.ForAll(Contract.Result<List<int>>(), i => i < limit));

        await Task.Delay(42);

        return Enumerable.Range(1, 10).ToList();
    }
}

Running ccrewrite on this class will fail with NullReferenceException at System.Compiler.Writer.cs line 1814.

Missing UpdateManifestVersion.exe

Its not possible to build the setup by running buildCC as it expects the executable UpdateManifestVersion.exe to exist in Microsoft.Research\common\bin.

ccdoc ArrayOutOfRangeException

Running ccdocgen on my project fails with this stacktrace

5>  "C:\Program Files (x86)\Microsoft\Contracts\Bin\ccdocgen.exe" "@obj\Debug\fooccdocgen.rsp"
5>  CCDoc failed with uncaught exception: Der Index war außerhalb des Arraybereichs.
5>  Stack trace:    bei Microsoft.Cci.Analysis.Stack`1.Pop()
5>     bei Microsoft.Cci.Analysis.DataFlowInferencer`2.SetupDataFlowFor(Instruction instruction)
5>     bei Microsoft.Cci.Analysis.DataFlowInferencer`2.DequeueBlockAndSetupDataFlow()
5>     bei Microsoft.Cci.Analysis.DataFlowInferencer`2.SetupDataFlowFor(IMethodBody methodBody)
5>     bei Microsoft.Cci.ILToCodeModel.SourceMethodBody..ctor(IMethodBody ilMethodBody, IMetadataHost host, ISourceLocationProvider sourceLocationProvider, ILocalScopeProvider localScopeProvider, DecompilerOptions options)
5>     bei Microsoft.Cci.MutableContracts.ContractExtractor.SplitMethodBodyIntoContractAndCode(IContractAwareHost host, ISourceMethodBody sourceMethodBody, PdbReader pdbReader)
5>     bei Microsoft.Cci.Contracts.LazyContractExtractor.GetMethodContractFor(Object method)
5>     bei Microsoft.Cci.Contracts.CodeContractsContractExtractor.GetMethodContractFor(Object method)
5>     bei CCDoc.CCDocContractHelper.TryGetMethodContract(CodeContractAwareHostEnvironment host, IMethodReference method, IMethodContract& methodContract, DocTracker docTracker)
5>     bei CCDoc.ContractVisitor.ContractPackager.PackageMethodContracts(IMethodDefinition method, Boolean isPure)
5>     bei CCDoc.ContractVisitor.Visit(IMethodDefinition methodDefinition)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IMethodDefinition method)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IEnumerable`1 methods)
5>     bei Microsoft.Cci.MetadataTraverser.TraverseChildren(ITypeDefinition typeDefinition)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(INamespaceTypeDefinition namespaceTypeDefinition)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IEnumerable`1 namespaceMembers)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(INestedUnitNamespace nestedUnitNamespace)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IEnumerable`1 namespaceMembers)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(INestedUnitNamespace nestedUnitNamespace)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IEnumerable`1 namespaceMembers)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(INestedUnitNamespace nestedUnitNamespace)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IEnumerable`1 namespaceMembers)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(INestedUnitNamespace nestedUnitNamespace)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IEnumerable`1 namespaceMembers)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IRootUnitNamespace rootUnitNamespace)
5>     bei Microsoft.Cci.MetadataTraverser.Traverse(IAssembly assembly)
5>     bei CCDoc.CCDoc.GetContracts(Options options, DocTracker docTracker)
5>     bei CCDoc.CCDoc.RealMain(String[] args)
5>     bei CCDoc.CCDoc.Main(String[] args)

Kind regards,
Michael

"Could not resolve type reference" for some iterator methods in VS2015

Any iterator methods which are explicitly implemented from an interface, and the interface contains multiple generic type arguments, causes a "Could not resolve type reference" error in the re-writer when built in Visual Studio 2015.
For example:

public class TestYield : IEnumerable<Tuple<int, int>>
{
    IEnumerator<Tuple<int, int>> IEnumerable<Tuple<int, int>>.GetEnumerator()
    {
        yield break;
    }

    IEnumerator IEnumerable.GetEnumerator()
    {
        yield break;
    }
}

fails with Could not resolve type reference: [TestContracts]TestContracts.TestYield.<System-Collections-Generic-IEnumerable<System-Collections-Generic-KeyValuePair<System-Int32\,System-Int32>>-GetEnumerator>d__0.

The root cause of this is the type name parser used by the re-writer to read attributes does not support reading type names with escaped characters. The Rosyln compiler is adding an IteratorStateMachineAttribute to the method pointing to a type with the name <System-Collections-Generic-IEnumerable<System-Collections-Generic-KeyValuePair<System-Int32,System-Int32>>-GetEnumerator>d__0, and the comma in the generic arguments gets escaped with a backslash in the IL.

Pull request incoming.

CodeContracts as NuGet package

When I worked with Azure build system I found that it doesn't support CodeContracts out of the box.
The same issue I run into on AppVeyor build system.

Since CodeContracts only support installation as MSI it was very annoying to make build work.
In deployment script I perform downloading of the installation package and run setup. Since setup is asynchronous without result there wasn't good way to check installation except of pulling directory or registry entries.
For Azure I hadn't even try =)

To make integration for build more elegant and native I created NuGet package which simply contains all the binaries and other files required for building. Upon installation it adds targets for CodeContracts rewriter explicitly to ensure it will be part of the build process.

The project lives as sources on GitHub here and as a package on NuGet.

It has been tested only on .Net 4.5 targets but I believe it should work with other that CC targets.

If you guys could could take care of it I can transfer the ownership to you.
Anyways, I support it by updating versions of CodeContracts.

Alternative active fork

Hi,

The offical codecontracts repository seems not to be maintained anymore. Is there an alternative fork that is maintained and moved forward?

Victor

Code Contract Editor Extensions for VS 2012 crash on start

Every time I start Visual Studio with the "Code Contracts Editor Extensions VS2012" enabled it crashes on start and asks me to send the logs. I am using:

Microsoft Visual Studio Ultimate 2013
Version 12.0.31101.00 Update 4

Microsoft .NET Framework
Version 4.6.00031

Is there a more up-to-date version for VS 2013 that does not crash? I have not been able to locate it.

Thanks,
Justin

CCRewriter removes Assert/Assume calls but not precondition checks from iterator blocks/async methods

I assume (pun intended) that this bug is related to #34.

Consider following code:

static bool Check()
{
    Console.WriteLine("Check!");
    return true;
}

private static IEnumerable<string> FooAsync1(string str)
{
    Contract.Assert(Check() && str != null );
    yield return str;
}

Rewriting this code with level < 4 (i.e. not in a Full mode) should remove Assert method call from the iterator block.

But in reality, ccrewriter removes anly method call itself, but leaves precondition check in the final IL code.

Running this code with Preconditions only, will print "Check" message on the screen.

The same behavior would be for async methods as well.

UPDATE: minor correction.
To reproduce this issue complexity of the expression matters but not where it was called (iterator block/async method/regular method):

private static void Foo(string str)
{
    // Check method would be called
    Contract.Assert(Check() && str != null);
    Console.WriteLine("Boo");
}

private static void Foo2(string str)
{
    // Call to Check method would be erased
    Contract.Assert(Check());
    Console.WriteLine("Boo");
}

With Preconditions only in Foo method Checkmethod would be called but inFoo2` method - not.

Unable to cast object of type 'System.Compiler.TypeParameter' to type 'System.Compiler.Class'.

When I have somewhat crazy class in my project like this:

public abstract class EntityDataAccessLayerPart<TDal, TDataContext, TItemBase, TSoftDelete> : EntityDataAccessLayerPart
    where TItemBase : class
    where TSoftDelete : class, TItemBase
    where TDal : EntityDataAccessLayer<TDataContext, TItemBase, TSoftDelete>
    where TDataContext : EntityContextBase

When I have code contracts enabled in my project I get following error when compiling

1>------ Build started: Project: RFERL.EntityFramework, Configuration: Debug-Fast Any CPU ------
1>  elapsed time: 1672ms
1>C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v12.0\Microsoft.CodeContracts.targets(397,5): warning : Contract reference assembly for project 'RFERL.CoreUtilities' not found. Select 'Build' or 'DoNotBuild' for Contract Reference in project settings.
1>  Reading assembly 'RFERL.EntityFramework' from 'C:\Code\common\RFERL.EntityFramework\obj\Debug-Fast\RFERL.EntityFramework.dll' resulted in errors.
1>      Unable to cast object of type 'System.Compiler.TypeParameter' to type 'System.Compiler.Class'.
1>ccrewrite : error : Rewrite aborted due to metadata errors. Check output window
1>  elapsed time: 789,191ms
1>C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v12.0\Microsoft.CodeContracts.targets(254,5): error MSB3073: The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite.exe" "@RFERL.EntityFrameworkccrewrite.rsp"" exited with code -1.
========== Build: 0 succeeded, 1 failed, 7 up-to-date, 0 skipped ==========

When I comment out part of the code like this

public abstract class EntityDataAccessLayerPart<TDal, TDataContext, TItemBase, TSoftDelete> : EntityDataAccessLayerPart
    where TItemBase : class
    where TSoftDelete : class, TItemBase
    where TDal : EntityDataAccessLayer//<TDataContext, TItemBase, TSoftDelete>
    where TDataContext : EntityContextBase

everything works

CC warns about missing contracts, even if contracts are there

Sometimes we get a warning like
Consider adding the postcondition Contract.Ensures(Contract.Result<System.String>() != null)
even though the contract it there.

I could reproduce it with this code:

public class Test2
{
    public string FullAppVersion
    {
        get
        {
            Contract.Ensures(Contract.Result<string>() != null);

            var sb = new StringBuilder();
            sb.Append("Version ");

            var assembly = Assembly.GetEntryAssembly();
            if (assembly != null)
            {
                var fvi = FileVersionInfo.GetVersionInfo(assembly.Location);
                sb.Append(fvi.ProductVersion);
            }

            return sb.ToString();
        }
    }
}

When removing the public keyword from the class or simplifying the code, the warning disappears.

FindOne Contract for System.DirectoryServices.DirectorySearcher

Contract is defined as:

Contract.Ensures(Contract.Result() != null);

But MSDN describes a null possibility:

If no entries are found to match the search criteria, a null reference (Nothing in Visual Basic) is returned

NullReferenceException with lambda in requires of contract class in VS2015

Ccrewrite fails with a NullReferenceException when a contract class contains a requires that has a lambda expression when compiled in Visual Studio 2015.

For example:

[ContractClass(typeof(FooContracts))]
public interface IFoo
{
    void Method(params string[] strings);
}

[ContractClassFor(typeof(IFoo))]
public abstract class FooContracts : IFoo
{
    public void Method(params string[] strings)
    {
        Contract.Requires(Contract.ForAll(strings, s => s.Length > 0));
    }
}

public class Foo : IFoo
{
    public void Method(params string[] strings)
    {
        Console.WriteLine(string.Join(", ", strings));
    }
}

Perform Runtime Contract Checking has to be enabled and not None.

I believe it is due to a change in how lambdas and closures are compiled by Rosyln. Something that may be related is a Debug.Assert failing in Foxtrot\Foxtrot\Utility.cs line 2320

ccrewrite incorrect pdb files, Causes problem in Open RIA Services Client Code generation (Code Contracts 1.7.11202.10)

We are using OpenRIA Services to generate silverlight client code from a server application.

When enabling Runtime Contract Checing : Full, the client code is not generated properly. There are a lot of missing entity properties in the generated code.

When debugging the OpenRiaServices.DomainServices.Tools project (during client code generation) it seems that when ccrewrite has done its job, the web-projects .pdb-file refers to the wrong .cs files.

This is the code used by OpenRiaServices to read the pdb. http://openriaservices.codeplex.com/SourceControl/latest#OpenRiaServices.DomainServices.Tools/Framework/Pdb/PdbSourceFileProviderFactory.cs

By checking the Read/Writes from MSBuild it seems that it reads the correct pdb atleast, but since the wrong files are refered from the pdb the properties for each entity is not found.

It seems like we are not the first to stumble upon this/similar problem : https://social.msdn.microsoft.com/Forums/en-US/e7a48a93-fe1d-4678-a150-6d025331388a/ria-services-client-code-generation-broken-after-installing-code-contracts-146031712?forum=codecontracts

This only happens when we enable Code Contracts. The pdb file refers to the correct files when Code Contracts is not enabled, and the client code is generated correctly.

(Also, i have tried to reinstall Code Contracts but same problem exists.)

(link to same issue on msdn : https://social.msdn.microsoft.com/Forums/en-US/1742d91f-a33e-41c9-b20f-5df5196267bc/ccrewrite-incorrect-pdb-files-causes-problem-in-open-ria-services-client-code-generation-code?forum=codecontracts)

SetSocketOption Contract Requirements are incorrect

For this overload, the contract requires IPV6 (41), but that is not the only valid way of calling this method.

https://github.com/Microsoft/CodeContracts/blob/master/Microsoft.Research/Contracts/System/System.Net.Sockets.Socket.cs#L313

Admittedly, the was this method can be called are not entirely straightforward to express in contract form.

http://msdn.microsoft.com/en-us/library/fs3sawaa%28v=vs.110%29.aspx

Code containing exception handling generates false warnings

namespace CCTestApp
{
[ContractClass(typeof(ServiceContract))]
public interface IService
{
IList GetSettings();
}

[ContractClassFor(typeof(IService))]
abstract class ServiceContract : IService
{
    IList<Setting> IService.GetSettings()
    {
        Contract.Ensures(Contract.Result<IList<Setting>>() != null);
        throw new NotImplementedException();
    }
}

public class Setting
{
    private readonly IService _service;
    private IList<Setting> _settings;

    public Setting(IService service)
    {
        Contract.Requires(service != null);
        _service = service;
    }

    public IList<Setting> SomeSettings
    {
        get
        {
            return _settings ?? (_settings = TryGetSettings());
        }
    }

    private IList<Setting> TryGetSettings()
    {
        try
        {
            return _service.GetSettings();
        }
        catch (EntityException)
        {
            // Database not available, just go with local settings.
        }
        return null;
    }
}

}

Even though TryGetSettings may return null if IService.GetSettings throws an exeption we get a warning that the SomeSettings should ensure Result<> != null

CCRewriter produces invalid IL on async method or iterator blocks

Code Contracts version: 1.7.11202.10 (reproduces on earlier versions as well).
Perform Runtime Contract Checking != Full
Debug/Release: both

Using CCRewrite with Perform Runtime Contract Checking not equals to Full with async method (or methods with iterator blocks) with complex Contract.Requires (that has II or && in it) provides invalid assembly. Using such an assembly leads to System.InvalidProgramExecution exception and peverify shows following error:

[IL]: Error: [PATHToExecutable\CcRewriterBug\bin\Release\CCRewriterBug.exe:
CcRewriterBug.Program+<FooEnumerable>d__3::MoveNext][offset 0x00000021] Stack underflow

Steps to reproduce:

static async Task FooAsync(string str)
{
   // Works fine with Contract.Requires(str != null);
    Contract.Requires(str != null && str.Length > 1);
    await Task.Delay(42);
}

or

static IEnumerable<string> FooEnumerable(string str)
{
    Contract.Requires(str != null && str.Length > 1);
    yield return str;
}

In latter case if Perform Runtime Contract Checking is not Full CCRewrite produces following IL in MoveMethod:

.method private final hidebysig newslot virtual 
    instance bool MoveNext () cil managed 
{
    .override method instance bool [mscorlib]System.Collections.IEnumerator::MoveNext()
    // Method begins at RVA 0x21ac
    // Code size 64 (0x40)
    .maxstack 2
    .locals init (
        [0] int32 CS$0$0000
    )

    IL_0000: ldarg.0
    IL_0001: ldfld int32 CcRewriterBug.Program/'<FooEnumerable>d__0'::'<>1__state'
    IL_0006: stloc.0
    IL_0007: ldloc.0
    IL_0008: switch (IL_001a, IL_0037)

    IL_0015: br IL_003e

    IL_001a: ldarg.0
    IL_001b: ldc.i4.m1
    IL_001c: stfld int32 CcRewriterBug.Program/'<FooEnumerable>d__0'::'<>1__state'
    IL_0021: pop // this instruction is invalid!
    IL_0022: ldarg.0
    IL_0023: ldarg.0
    IL_0024: ldfld string CcRewriterBug.Program/'<FooEnumerable>d__0'::str
    IL_0029: stfld string CcRewriterBug.Program/'<FooEnumerable>d__0'::'<>2__current'
    IL_002e: ldarg.0
    IL_002f: ldc.i4.1
    IL_0030: stfld int32 CcRewriterBug.Program/'<FooEnumerable>d__0'::'<>1__state'
    IL_0035: ldc.i4.1
    IL_0036: ret

    IL_0037: ldarg.0
    IL_0038: ldc.i4.m1
    IL_0039: stfld int32 CcRewriterBug.Program/'<FooEnumerable>d__0'::'<>1__state'

    IL_003e: ldc.i4.0
    IL_003f: ret
} // end of method '<FooEnumerable>d__0'::MoveNext```

Format source code

We need to do this. Current code is not formatted very well...

Add license file

Currently the license is specified only in headers of source files. It would be helpful to have a license file in the repository root folder so it's immediately clear to new users.

ccrewrite adds invalid source reference to PDB file

The source for the project is at https://tomstoolbox.codeplex.com/SourceControl/latest (Feature/Default branch, Desktop module)

When "Perform Runtime Contract Checking (Preconditions)" is on, an invalid source file reference is added to the .pdb file.

The class is TomsToolbox.Desktop.DependencyObjectExtensions.DependencyPropertyEventWrapper`1, which implements TomsToolbox.Core.INotifyChanged.

Without the rewriter the pdb contains a link to the correct source file, but when enabling the rewriter the pdb contains an additional link to the source file of TomsToolbox.Core.INotifyChanged, which is in a different project!

Now the NuGet package manager can't find this
source file, since it's from another project, and the NuGet symbol package is considered invalid.

Malfromed Contract. Found Requires after assignment

After abbreviators started to work, we get the error

Malfromed Contract. Found Requires after assignment.

for the following method:

[ContractAbbreviator]
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "value")]
[SuppressMessage("Microsoft.Usage", "CA1801:ReviewUnusedParameters", MessageId = "userMessage")]
public static void NotDefault<T>(T value, string userMessage)
{
    Contract.Requires<ArgumentException>(!EqualityComparer<T>.Default.Equals(value, default(T)), userMessage);
}

If method's body is inlined as a usual CodeContract, or abbreviator is used within the same assembly no errors appear.

Update
This error occurs only for enum types.

Add treat warnings as error option for ccrewriter

Please add an option for the ccrewriter to treat warnings as errors. Without that I can't prevent checkins with contract warnings.

Create a new set of lables for project.

What do you think about creating a new sot of labels for CC? Current one does not look consistent.
Newly created set may be similar to the one defined for NuGet.

Support for VS2015

Can we add support for VS2015? I use it for most of my projects but need to keep 2013 around for projects that use CodeContracts.

Microsoft.CodeContracts.targets reverts to .NET v3.5 reference assemblies for 4.5.2

There's no When block for .NET 4.5.2, so the CodeContractsReferenceAssemblyLibPath falls back to v3.5 contracts for projects that target 4.5.2. Consider adding a block for 4.5.2, a StartsWith('4.5') check can work for any 4.5 release, defaulting to 4.5 rather than 3.5, or using Substring() on the TargetFrameworkVersion to avoid hard-coded versions.

Support VS2013 for CC Editor Extensions

Editor Extensions throw an exception when only VS2013 is installed on a machine. Please provide a new extension that supports VS2013.

Even when registering the missing VS2012 dlls in the GAC the intellisense support to show contracts doesn't work.

CCRewrite fails with NRE on async method with Ensures.ForAll with captured params because forwarder is null

There is another issue with CCRewrite when Contract.Ensures contains Ensures.ForAll with captured lambda. Related issue #69.

Following code lead to another NRE:

  class NonGen {
        public async Task<List<int>> FooAsync(int limit)
        {
            Contract.Ensures(Contract.ForAll(Contract.Result<List<int>>(), i => i < limit));

            await Task.Delay(42);

            return new List<int>{1, 2, 3, 4, 5, 6, 7, 8, 9, 10};
        }
  }

Trying to use this method lead to NRE at Rewriter.cs:3994:

public override Expression VisitLocal(Local local)
{
    if (HelperMethods.IsClosureType(this.declaringType, local.Type))
    {
        MemberBinding mb;
        if (!closureLocals.TryGetValue(local, out mb))
        {
            // Next line will fail, because this.forwareder is null!
            var closureField = new Field(this.closureClass, null, FieldFlags.Public, local.Name, this.forwarder.VisitTypeReference(local.Type), null);
            this.closureClass.Members.Add(closureField);
            mb = new MemberBinding(this.checkMethod.ThisParameter, closureField);
            closureLocals.Add(local, mb);

            // initialize the closure field
            var instantiatedField = GetMemberInstanceReference(closureField, this.closureClassInstance);
            this.ClosureInitializer.Statements.Add(new AssignmentStatement(new MemberBinding(this.ClosureLocal, instantiatedField), local));

        }
        return mb;
    }
    return local;
}

This issue is similar to #69 but the reason is different. This time the root cause is following code in Rewriter.cs (in `EmitAsyncClosure):

if (from.IsGeneric)
            {
                this.closureClass.TemplateParameters = new TypeNodeList();
                var parentCount = this.declaringType.ConsolidatedTemplateParameters == null ? 0 : this.declaringType.ConsolidatedTemplateParameters.Count;
                for (int i = 0; i < from.TemplateParameters.Count; i++)
                {
                    var tp = HelperMethods.NewEqualTypeParameter(dup, (ITypeParameter)from.TemplateParameters[i], this.closureClass, parentCount + i);

                    this.closureClass.TemplateParameters.Add(tp);
                }
                this.closureClass.IsGeneric = true;
                this.closureClass.EnsureMangledName();
                this.forwarder = new Specializer(this.declaringType.DeclaringModule, from.TemplateParameters, this.closureClass.TemplateParameters);
                this.forwarder.VisitTypeParameterList(this.closureClass.TemplateParameters);

                taskType = this.forwarder.VisitTypeReference(taskType);

            }
            else
            {
                // In this case forwarder is NULL!
                this.closureClassInstance = this.closureClass;
            }
```c#

False positive: precondition is redundant

As described in this Stackoverflow post the following code:

public int Foo(int a)
{
    if (a >= 0) throw new ArgumentException("a should be negative", "a");
    Contract.EndContractBlock();
    return a;
}

gives the following warning during static checking: CodeContracts: Suggested requires: This precondition is redundant: Consider removing it. Are you comparing a struct value to null?

when compiled with warning level 2 or higher. The corresponding Contract.Requires() does not produce the same error.

This happens with the newest version at this time (1.7.11202.10) under Visual Studio 2013 Professional at least.

CCR solution references non-existent projects

The solution CCR.sln references a set of projects which are not part of this repository.

CodeContract static analyzer fails the build for no specific reason

I have an issue where the static analyzer will claim that the build has failed without actually specifying any build errors. 'Fail build on warning' is disabled.

I do get one warning however:

******\packages\Microsoft.Net.Http.2.2.29\lib\portable-net40+sl4+win8+wp71+wpa81\System.Net.Http.dll(1,1): warning : CodeContracts: Could not find the method/type 'System.Diagnostics.Contracts.PureAttribute' in assembly '******\packages\Microsoft.Net.Http.2.2.29\lib\portable-net40+sl4+win8+wp71+wpa81\System.Net.Http.dll'

To me this warning doesn't make sense. Why is it looking for System.Diagnostics.Contracts.PureAttribute in System.Net.Http?

This is the build log: http://pastebin.com/1Fu4REbr

It also claims that it ran the test on the dll, and that the dll is located in C:\Windows\System32, which is not correct as far as I know, since the process probably does not have write access to C:\Windows\System32, and there is no dll of that name there.

ILMerge does not generate body of methods with delegates/lambda compiled by roslyn.

ccrewriter compiled under VS2015 fails on startup with the following error:
Unhandled Exception: System.TypeLoadException: Could not load type 'Microsoft.Contracts.Foxtrot.Driver.Program' from assembly 'ccrewrite, Version=1.8.10107.11, Culture=neutral, PublicKeyToken=188286aac86319f9' because the method 'InternalMain' has no implementation (no RVA).

It turns out that this is the case for all the method with delegate/lambda in body and only for assemblies produced by roslyn. Much worse scnario is for void returning methods as the loader do not raise an exception for them.

There are few ways we can go:

1. Get an updated version of ILMerge from Mr. @mike-barnett.
2. Locate and replace all the delegate/lambda code in libraries used with ILMerge.
3. Drop ILMerge usage.

Build procedure shall be redefined.

Currently there are some areas in build procedure that are far from optimal. For example:

• some configurations are not used anymore (academic, internal, release).
• Editor Extension is excluded from command line build.
• some parts of the buildMSI10.xml are not used.
• build stages are blurred.

We should define a new build procedure. This may also require a changes in directory structure.

Enumerable lazy checks

I found that Contract.ForAll enumerates it's argument when perform checking post- or pre- conditions. Such behavior could produce unexpected multiple enumeration in some cases where it isn't desirable. For example:

• enumerable has no ending (infinite sequence)
• generator has side effects
• generator is resource eager

I propose to generate substitution for parameters/arguments that checks conditions lazily.

public IEnumerable<int> Generator()
{
    Contract.Requires(Contract.ForAll(Contract.Result<IEnumerable<int>>(), x => x > 0))

    while (...)
        yield return ...;
}

This code should be rewritten to validate once the values will be produced.
Let's say we have captured the result into result of type IEnumerable<int> from code above. Then instead of enumerating it, need to replace with result.Select(x => { contract_check(x > 0); return x; }).
Same thing could be done with preconditions.
There's still an option to check by enumerating when the argument is array or List (IList doesn't work, because it also could be generated).

Returing constant in interface implementation suggests impossible contracts

when implementing an interface method like this:

    bool ICollection.IsSynchronized
    {
        get
        {
            return false;
        }
    }

I get a CC warning:

Warning 12 CodeContracts: Consider adding the postcondition Contract.Ensures(Contract.Result<System.Boolean>() == false); to provide extra-documentation to the library clients

However since this is an interface implementation, I can't add contracts here.

Update/uninstall leaves VS2013 extension behind

If you uninstall code contracts, either manually or by installing a new version, the VS2013 extension stays installed or stays at the old version. The whole folder C:\Program Files (x86)\Microsoft Visual Studio 12.0\Common7\IDE\Extensions\Microsoft\CodeContracts isn't removed.

Method System.Diagnostics.Contracts.Contract.Requres<T> has missing Conditional attribute

Method System.Diagnostics.Contracts.Contract.Requres<T> should be decorated with [Conditional("CONTRACTS_FULL")].
Right now when using Code Contracts and turn off runtime checking, in place where Contract.Requires<T> used, produced exception like that:

An assembly (probably "TestAssembly") must be rewritten using the code contracts binary rewriter (CCRewrite) because it is calling Contract.Requires and the CONTRACTS_FULL symbol is defined. Remove any explicit definitions of the CONTRACTS_FULL symbol from your project and rebuild. CCRewrite can be downloaded from http://go.microsoft.com/fwlink/?LinkID=169180. After the rewriter is installed, it can be enabled in Visual Studio from the project's Properties page on the Code Contracts pane. Ensure that "Perform Runtime Contract Checking" is enabled, which will define CONTRACTS_FULL.