ReSharper - Possible Zero Assignment When Using Microsoft.Contracts

Question

Is there a way to tell ReSharper that a null reference will not occur due to contract construction Requires verification? For example, the following code raises a warning ( Possible 'null' assignment to entity marked with 'NotNull' attribute ) in ReSharper on lines 7 and 8:

 private Dictionary<string, string> _Lookup = new Dictionary<string, string>(); public void Foo(string s) { Contract.Requires(!String.IsNullOrEmpty(s)); if (_Lookup.ContainsKey(s)) _Lookup.Remove(s); } 

What is really strange is that if you delete the Contract.Requires(...) , the ReSharper message will disappear.

Update

I found a solution through ExternalAnnotations, which Mike also mentioned below. Here is an example of how to do this for a function in Microsoft.Contracts:

• Create a directory under Microsoft.Contracts in the ExternalAnnotations ReSharper directory.
• Next, create a file called Microsoft.Contracts.xml and write it like this:

 <assembly name="Microsoft.Contracts"> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> </assembly> 

• Restart Visual Studio and the message will disappear!

Answer 1

Note : with the current RAP 8.0 EAP, this functionality is enabled.

---

Here's a solution for the current (i.e. .NET 4.0) version of code contracts:

Inside ...\ExternalAnnotations\mscorlib\Contracts.xml add the following:

 <assembly name="mscorlib"> <member name="M:System.Diagnostics.Contracts.Contract.Assert(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assert(System.Boolean, System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assume(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assume(System.Boolean, System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires``1(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires``1(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Invariant(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Invariant(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> </assembly> 

Answer 2

I would like to add that for people who write their own approval methods, etc., you can include these attributes without an external XML file. In Visual Studio, go to ReSharper > Options > Code Annotations and click the Copy default implementation to clipboard button. Then create a new file (anywhere in your solution) and paste the code from the clipboard. Now you can create such methods:

 public class Require { [AssertionMethod] public static void That( [AssertionCondition(AssertionConditionType.IS_TRUE)] bool requiredCondition, string message = null) { ... } ... } 

Now, any call to Require.That(a != null) will tell ReSharper that you cannot pass this line if a is null. Unlike the ExternalAnnotations method, this will work for those who use your methods, without any additional work on their part.

Update

Resharper has changed its contract annotation model since version 7. Here's what the following method would look like:

 public class Require { [ContractAnnotation("requiredCondition:false => halt")] public static void That( bool requiredCondition, string message = null) { ... } ... } 

Answer 3

I think you can, but this is not trivial. Take a look at Resharper online help for code annotation

They annotated the BCL classes and the NUnit framework (and much more) to improve Resharpers code validation capabilities.

For example, using NUnit, they are annotated using the AssertionMethodAttribute attribute. This suggests checking the Resharpers code that if you passed Assert.IsNotNull (foo); then foo should not be zero and will no longer give a warning "Possible" null "assignment ...".

You can create an xml file annotating the Contracts.Requires method to indicate that it is exactly the same as Assert.

Answer 4

The reason the message goes away when you delete the statement is because R # defaults to "optimistic" mode. It is assumed that everything is not null until you do something that indicates that it may be null. What happens when you add a call to String.IsNullOrEmpty . You state that s may be null. He just doesn't know that the Contract.Requires method will stop executing if that happens, but you decided with the annotation.

In R # 5.0, you can go into a pessimistic mode that takes the worst in every corner.

Answer 5

I took XML Porges and added annotations for the Assert and Assume methods. I will answer this question if other people want to add more methods.

 <assembly name="mscorlib"> <member name="M:System.Diagnostics.Contracts.Contract.Assert(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assert(System.Boolean, System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assume(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assume(System.Boolean, System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires``1(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires``1(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Invariant(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> <member name="M:System.Diagnostics.Contracts.Contract.Invariant(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <parameter name="condition"> <attribute ctor="M:JetBrains.Annotations.AssertionConditionAttribute.#ctor(JetBrains.Annotations.AssertionConditionType)"> <argument>0</argument> </attribute> </parameter> </member> </assembly> 

Answer 6

Resharper has changed its contract annotation model from version 7.

You need another file. New location (I think only for Metro applications): "C: \ Program Files (x86) \ JetBrains \ ReSharper \ v7.1 \ Bin \ ExternalAnnotes \ .NETCore \ System.Diagnostics.Contracts \ Contracts.xml"

I am using Visual Studio 2012 and .Net 4.5 and Resharper 7.1.

Content:

 <assembly name="System.Diagnostics.Contracts"> <member name="M:System.Diagnostics.Contracts.Contract.Assert(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assert(System.Boolean, System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assume(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Assume(System.Boolean, System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires``1(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Requires``1(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Invariant(System.Boolean)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> <member name="M:System.Diagnostics.Contracts.Contract.Invariant(System.Boolean,System.String)"> <attribute ctor="M:JetBrains.Annotations.AssertionMethodAttribute.#ctor"/> <attribute ctor="M:JetBrains.Annotations.ContractAnnotationAttribute.#ctor(System.String)"> <argument>condition:false=&gt;halt</argument> </attribute> </member> </assembly> 

Answer 7

TL; DR - Add the conditional compilation symbol CONTRACTS_FULL to your project.

The Contract.Requires(...) method is empty and disabled, unless you enable and use the Code Contacts rewriter. By starting the rewriting program manually or (usually) enabling it through the properties of the Visual Studio project, you save the Contract.Requires(...) code in the compiled and rewritten binaries. You know that the code will work, and ignoring the Resharper warning, you can run it and test it.

What is the problem then? Resharper does not know that code contracts are executed, since they are really only entered at compile time (post-). According to Resharper, it is disabled in the same way that the DEBUG preprocessor symbol works and how Visual Studio selects areas of your code that will not be part of your compiled binaries.

 #ifdef DEBUG Console.WriteLine("I'm in DEBUG mode, so this is probably a Debug build."); #else Console.WriteLine("Let assume this is a Release build."); #endif 

According to the Code Contracts user manual (chapter 2, first paragraph) and the source code in ContractExtensions.cs (included in the Code Contracts installation folder), CONTRACTS_FULL must be set before compiling with this. Contract methods are actually implemented using [ConditionalAttribute("CONTRACTS_FULL")] and are ignored (not included at compile time) if the flag is not set. Resharper respects this flag and assumes that the function will not work if it is not installed.

 [ConditionalAttribute("CONTRACTS_FULL")] public static void Requires(bool condition) { ... } 

Solution: Add the CONTRACTS_FULL conditional compilation symbol to your project. See Using Visual Studio Code Contracts and Henning Krause Resharper .

_{(source: infinitec.de )}

The Resharper team has been notified; When analyzing the code, the parameters on the project properties tab of the project "Contracts by code" , Support for contracts by Microsoft code are not taken into account .