CODEWITHSUNDEEP
c#static-analysiscode-contracts
luiscubal
luiscubal

Reputation: 25161

Code Contracts static analyzer doesn't detect trivial contract violation

I have this code:

using System;
using System.Diagnostics.Contracts;

namespace TestCodeContracts
{
    class Program
    {
        public static int Divide(int numerator, int denominator, out int remainder)
        {
            Contract.Requires<ArgumentException>(denominator != 0);
            Contract.Requires<ArgumentException>(numerator != int.MinValue || denominator != -1, "Overflow");
            Contract.Ensures(Contract.Result<int>() == numerator / denominator);
            Contract.Ensures(Contract.ValueAtReturn<int>(out remainder) == numerator % denominator);

            remainder = numerator % denominator;
            return numerator / denominator;
        }

        static void Main(string[] args)
        {
            int remainder;
            Console.WriteLine(Divide(10, 6, out remainder));
            Console.WriteLine(Divide(5, remainder, out remainder));

            Console.WriteLine(Divide(3, 0, out remainder));

            Console.Read();
        }
    }
}

On the first Divide call, if I replace 6 by 0, then the static analysis correctly warns against it.

If I replace 6 by 5, then I (correctly) get a warning on the second Divide call.

However, no matter what, I never get any warnings on the third Divide call. Instead, I just get a runtime error.

Why is the static analyzer unable to detect that the third line is a contract violation?

I am using Visual Studio 2012, on Windows 8 64-bit. The code contracts is Microsoft Code Contracts (devlabs_TS) 1.4.51019.0 for .NET (which seems to be the latest version as of December 2012).

Upvotes: 2

Views: 360

Answers (2)

luiscubal
luiscubal

Reputation: 25161

I posted this in the code contracts forum. It is confirmed that this is indeed a bug and that it will be fixed.

The bug is that the static verifier thinks that the Divide(3, 0... ) is unreachable

(...)

We will fix the bug.

Upvotes: 3

Mightymuke
Mightymuke

Reputation: 5144

This is an interesting problem.

I finally simplified Divide down to this:

public static int Divide(int numerator, int denominator)
{
    Contract.Requires<ArgumentException>(denominator != 0);
    return numerator / denominator;
}

This throws the correct warning:

static void Main(string[] args)
{
    Console.WriteLine(Divide(10, 10));
    Console.WriteLine(Divide(10, 0));
}

Note that I found you have to generally rebuild rather than build, even with only one project. There must be code contract artefacts that get cleaned up on the rebuild.

This doesn't throw the warning:

static void Main(string[] args)
{
    Console.WriteLine(Divide(10, 9));
    Console.WriteLine(Divide(10, 0));
}

The only way I could trigger the warning was if the denominator for the first divide was 10 (and it obviously also worked when it was 0).

It does seem like a bug - I'd send an email to the code contracts team and see what they say.

Upvotes: 1

Related Questions