Why am I flooded with bogus contract messages?

Question

A while back I decided to explore Code Contracts.  While there are some very definite problems with the system I found it to generally be a better answer than using Asserts to check data.

I took a project I was working on and started implementing contracts.  It caught a bunch of cases where I had failed to check for bad results, some of which actually warranted better error handling.

I finally cleared the last warning and it decided to throw a fit, warnings all over the place that weren't legit.  I put it aside, today I downloaded the new version and tried it again.

I'm looking at 52 warnings--every last one of which is utterly bogus.  Every last one of them involves a situation where the designer created a visual component and then a later line refers to that component--the majority of the flagged lines being in the designer files but some are in my code.

An example:

this.GoButton = new System.Windows.Forms.Button();

// Lines which will not alter this.GoButton

this.GoButton.Location = new System.Drawing.Point(50, 200);

The second line is flagged as possibly calling a method on a null reference 'this.GoButton'.

Previously I had to use a lot of Contract.Assert()s to deal with similar cases in my code that had a similar structure--an object was created, something else was done that couldn't alter the existence of the object and then a reference to it got flagged as possibly null.

Furthermore, I have 352 messages from this compile suggesting conditions, many of which already exist.  I turned off *ALL* the "suggest <x>" flags, they appear anyway.

Answer 1

Hi,

Warnings for designer-generated code is normal.  Designers don't specify any contracts, such as Contract.Invariant(GoButton != null), so the static checker is doing the right thing and warning you about potential bugs in your code.

You could try specifying invariant contracts for designer-generated code yourself in a partial class, but it probably won't work because designers generally rely on an Initialize method to assign fields, which means that the invariants are broken in constructors.

Depending on the platform, you may be able to specify invariants in the form of implications, such as the following:

Contract.Invariant(!IsInitialized || GoButton != null)

Though you may still get warnings because designer-generated methods don't have contracts to ensure that IsInitialized == true.

Essentially, the problem isn't with code contracts.  The problem is that designer-generated code isn't designed to support invariants.

As such, I often find that the best course of action is to suppress all static checking in designer-generated classes:

[ContractVerification(false)]
partial class MyGUI { ... }

Unfortunately, it means that you won't get any help from the static checker in your partial class either.

Hopefully in the future, MS designers will support code contracts out-of-the-box.

- Dave

---

http://davesexton.com/blog

Answer 2

Hi,

Warnings for designer-generated code is normal.  Designers don't specify any contracts, such as Contract.Invariant(GoButton != null), so the static checker is doing the right thing and warning you about potential bugs in your code.

Huh?  After a new how can an object be null?  It either creates the object or throws an exception, in no case should you be able to get past the line without it being assigned.

Answer 3

Hi,

> // Lines which will not alter this.GoButton

This is why.  You know that these lines won't alter GoButton, but the static checker doesn't because there aren't any contracts that prevent GoButton from being re-assigned as a side-effect.  In other words, GoButton is not a read-only field with an invariant contract that prevents it from being re-assigned.  It can be changed at any time.

- Dave

---

http://davesexton.com/blog

Answer 4

Hi,

Here's a simple example to illustrate my previous point:

using System.Diagnostics.Contracts;

namespace ConsoleApplication1
{
	class Example
	{
		private object obj;

		void Foo()
		{
			obj = new object();

			Contract.Assert(obj != null);

			Bar();

			Contract.Assert(obj != null);	// Warning 1 CodeContracts: assert unproven
		}

		void Bar()
		{
		}
	}
}

- Dave

---

http://davesexton.com/blog

Answer 5

Hi,

> // Lines which will not alter this.GoButton

This is why.  You know that these lines won't alter GoButton, but the static checker doesn't because there aren't any contracts that prevent GoButton from being re-assigned as a side-effect.  In other words, GoButton is not a read-only field with an invariant contract that prevents it from being re-assigned.  It can be changed at any time.

- Dave

---

http://davesexton.com/blog

In other words the checker doesn't evaluate if a field could get stomped or not.

Is this something that is going to be remedied in the future or should I just go back to Asserts?

Answer 6

Hi, 

> In other words the checker doesn't evaluate if a field could get stomped or not.

That's correct.  The static checker analyzes one method at a time and relies on the invariant contracts that you specify in the class and the pre- and post-condition contracts that you specify in other methods to determine their side-effects.  Contracts are the focus here.

> Is this something that is going to be remedied in the future or should I just go back to Asserts?

Generally, you should add contracts to fix problems like this.  It doesn't need to be "remedied" because it's not a problem with CC.  It's just a problem with missing contracts.

Of course, you can't always satisfy the static checker when dealing with designer-generated code by simply adding contracts, as I've described previously in this discussion.  Thus, you may have to resort to calling Contract.Assume wherever needed or you can simply disable verification by applying ContractVerificationAttribute to any method or class, as was previously suggested.

Referring back to my previous code example, if we don't specify any contracts on the Bar method then the static checker can't know whether the shared obj field has changed.  We can resolve this problem by adding a single contract to Bar:

using System.Diagnostics.Contracts;

namespace ConsoleApplication1
{
	class Example
	{
		private object obj;

		void Foo()
		{
			obj = new object();

			Contract.Assert(obj != null);

			Bar();

			Contract.Assert(obj != null);	// No warnings
		}

		void Bar()
		{
			Contract.Ensures(obj == Contract.OldValue(obj));
		}
	}
}

You may be able to solve your particular problem in a similar way, regardless of whether the field is designer-generated or not.  What matters is the side-effects of the other methods that you're calling.

Note that in some cases you can't add contracts because the methods aren't yours; i.e., they could be FCL methods.  In that case, calling the method could theoretically raise an event that your code handles and mutates the field, thus the complexity of how your internal state can be changed increases.

For this reason, I find immutability much easier to work with.  Obviously this doesn't apply to designer-generated code, which is why I often decided to not waste any time and simply apply ContractVerificationAttribute to the entire class.

- Dave

---

http://davesexton.com/blog

Answer 7

It sounds like it's a good idea that's not ready to be used.  I'll check back in something like a year.

Answer 8

Hi,

What do you expect to be different in a year?  How can the static checker be improved in your opinion?

- Dave

---

http://davesexton.com/blog

Answer 9

Hi,

Note that you can apply good coding practices to get the most out of code contracts.  For example, you can implement the MVVM pattern, which is especially useful in a WPF application.  It helps to avoid most of the warnings that you're getting because you wouldn't be coding against designer-generated members.  Instead, you should use XAML bindings against properties in a view model class.  Since you have complete control over the view model, you can specify all necessary contracts without any issues.

- Dave

---

http://davesexton.com/blog

Answer 10

Hi,

What do you expect to be different in a year?  How can the static checker be improved in your opinion?

- Dave

---

http://davesexton.com/blog

It could look at what a routine *COULD* modify.  If there are no writes to a field that can be reached by a routine (or at least in a reasonable fashion--ignore callbacks) then the field will remain as it was.

Some other improvements:

Invariant methods should only apply after the constructors are done--it should be acceptable to put an invariant in an abstract parent that will only be satisfied by the children.

I would like to see some support for lazy instantiation here but I'm not sure what it should look like.

Perhaps I missed it but I see no way to apply contracts to items in a collection--the biggie I noticed was whether there were nulls in it.

I also see no way for a contract to declare that an item in a class exists.  (This isn't inherently a violation of the Law of Dementer--many classes exist which are basically a collection plus supporting routines.  Such classes usually expose that collection.)

Also:

Write out the analysis of a file somewhere (probably with the source file) and only redo the analysis if something changes.  The current system is simply too slow.

Answer 11

Hi,

Your concerns are mostly valid, though some of them have already been implemented.

> It could look at what a routine *COULD* modify [snip]

That could depend upon complex runtime state and control flow, which is obviously going to be difficult if not impossible for a static analysis tool, to any significant extent, except perhaps in the simplest of cases (such as a single method, assuming that all calls may mutate mutable state).

I think you may have misunderstood the point of code "contracts".  The idea is to provide an explicit specification through contracts, which the static checker validates per method.  This makes it much easier to detect null references.  By default, the static checker warns you that a reference may be null unless it can prove otherwise based on local analysis of the current method and contracts that you've specified for any members used within the current method.  Eric mentions Code Contracts in the link above, but he doesn't indicate how it does a good job at this kind of analysis: contracts.

Read more about design by contract.

Furthermore, it's often quite easy to add contracts to solve your original problem, as I've shown above in my code example by adding a single contract to the Bar method (one of perhaps several solutions).  Unfortunately, designer-generated code is generated, which makes it difficult to specify more restrictive contracts.  Code generators should specify contracts themselves, but alas the WinForms code generator doesn't.  Applying better patterns to your code, such as MVVM, gives you more control over contracts.

> Invariant methods should only apply after the constructors are done [snip]

I believe that this has already been discussed in the forums and considered by the CC team, IIRC.  I guess this kind of "loose" invariant was never added as a feature because it's not very common in practice.

> I would like to see some support for lazy instantiation here but I'm not sure what it should look like.

It's pretty easy to apply contracts to lazy initialization already.  Implication contracts are useful for this purpose: 

Contract.Invariant(!initialized || field != null);

> Perhaps I missed it but I see no way to apply contracts to items in a collection--
> the biggie I noticed was whether there were nulls in it.

I believe this feature already exists, though the static checker is limited in its use.  It supposedly works for simple null checks.  There used to be a property that had to be enabled in the project, but I don't see it as of the latest release (or I'm just not looking for correct name).

For example:

Contract.Requires(Contract.ForEach(args, a => a != null));

> I also see no way for a contract to declare that an item in a class exists [snip]

Could you be more specific please?  I don't understand what you want.

> only redo the analysis if something changes

This feature already exists.  Just enable the Cache Results setting in your project.

- Dave

---

http://davesexton.com/blog