Summary

This is the first major community-driven release of the DotNet CodeContracts. This release addresses a lot of pending issues with installer, new IL patterns introduced by Roslyn Csc compiler, and more reasonable implementation of the postconditions in async methods, a lot of changes in the BCL contracts and more.

Nuget Package

DotNet.CodeContracts at nuget.org

Improvements and new features

• Proper implementation of async methods postconditions. Now async postconditions are implemented via call to ContinueWith method that checks a postcondition only when task finishes successfully (more details at #278).
• Postcondition for async method now runs synchronously to reduce additional overhead (#275).

Updated contracts for BCL types

• Added missing contracts in System.Linq.Expressions.Expression (#171)
• Contracts for System.Reflection.CustomAttributeExtensions (#180)
• String.IndexOfAny contract incorrect (#200)
• False contract assumption encountered on System.Decimal.op_Explicit (#203)
• Added missing contracts in Directory class (#251)
• Add missing contracts in System.Windows.Input.InputManager (#285)
• Add missing contracts in System.Windows.Data.MultiMinding (#286)
• Extend postcondition on Path.GetTempFileName (#305)
• Contracts for System.Version (#318)
• Contract reference assemblies for .NET Framework (#291)
• Update System.Threading.Tasks.Task for NET4.5/4.6 (#296)
• Add contracts for System.OperatingSystem (#306)

Bug fixes

Installation + VS Integration issues

• Update/uninstall leaves VS2013 extension behind (#7)
• Installer creates a C:\VS11Root folder (#8)
• Static checker warnings showing in the wrong pane is VS2015 (#166)

Async + Iterators + VS2015 issues

• Async/iterator issue in async without await (#172)
• Static checker: recognizing cached anonymous delegate fields produced by Roslyn (#182)
• ccrewrite produces an incorrect type name in
• Static checker can't prove ForAll on Roslyn-compiled inline arrays (#204)
• BadImageFormatException when using Contract.Ensures in async method, that returns task without any await (#235)
• NullReferenceException in ccrewrite-generated code (#191)
• Contract.Require(x != null) gets translated in!(x <= null)` in the documentation rewritten by CC (#307)
• Using capturing precondition in async method in struct lead to invalid IL (#168)

Other bug fixes

• Sql exceptions: String or binary data would be truncated (#165)
• Malformed Contract. Found Requires after assignment (#29)
• Bad application of visibility rules on method parameter attribute (#273)

Misc

• Code was reformatted to follow well-known .NET coding conventions using StyleCopAnalyzers
• All unit tests were migrated from MS Test to Xunit
• CodeContracts as NugetPackage (#13)

Acknowledgements

Thank you goes to all of the following users, who contributed feedback, bug reports, code submissions, testing, and reviews which helped in this release. In alphabetical order by username.

• @asvishnyakov
• @fedotovalex
• @panacekcz
• @jterry75
• @hubuk
• @mariachris
• @mike-barnett
• @ndykman
• @sharwell
• @tom-englert
• @yaakov-h