Code Contracts Forum

Why inferring methodensures doesn't work here?

Wed, 25 Nov 2009 19:50:46 Z

Compiled with option "-infer methodensures":

    class Program
    {
        static void Main(string[] args)
        {
            string s = Test();
            Contract.Assert(s.Length < 10); // assert unproven
        }

        static string Test()
        {
            string s = new string('x', 7);
            Contract.Assume(s.Length < 10);
            return s;
        }
    }

False Positive: CodeContracts: Suggested precondition: Contract.Requires(!string.IsNullOrEmpty(value));

Sat, 21 Nov 2009 07:53:10 Z


 <Extension()> Public Function IsEmailAddress(ByVal value As String) As Boolean
        If value = "" Then Return False
        Try
            Dim temp = New MailAddress(value)
            Return True
        Catch ex As FormatException
            Return False
        End Try
    End Function

ContractsRuntime recursion guard optimization

Sun, 15 Nov 2009 12:20:04 Z

The recursion guard is not necessary if contract statements doesn't call any methods, for example:

    if (__ContractsRuntime.insideContractEvaluation <= 4)
    {
        try
        {
            __ContractsRuntime.insideContractEvaluation++;
            __ContractsRuntime.Requires(arg1 >= 0, null, "arg1 >= 0");
            __ContractsRuntime.Requires(arg1 <= 127, null, "arg1 <= 127");
        }
        finally
        {
            __ContractsRuntime.insideContractEvaluation--;
        }
    }

It will be ok to just leave __ContractRuntime.Requires here:

            __ContractsRuntime.Requires(arg1 >= 0, null, "arg1 >= 0");
            __ContractsRuntime.Requires(arg1 <= 127, null, "arg1 <= 127");

Runtime contract checking is not for debugging only and would be nice not to have any unnecessary overhead in deployed code. There is no such guard in constructors already. Maybe it's not difficult to slightly optimize other methods where the guard is not required.

False positive on LinkedList.First

Wed, 25 Nov 2009 03:40:36 Z

This block warns that m_List.First may return a null.

Private ReadOnly m_List As New LinkedList(Of T)

        Public Function TryDequeue(ByRef value As T) As Boolean
            SyncLock m_Lock
                If m_List.Count > 0 Then
                    value = m_List.First.Value
                    m_List.RemoveFirst()
                    Return True
                Else
                    value = Nothing
                    Return False
                End If
            End SyncLock
        End Function

False Positive on read-only fields

Wed, 25 Nov 2009 03:33:29 Z

The field is declared as shown below. Whenever I try to read from that field, I get a "possibly calling a method on a null reference" warning.

Private

ReadOnly m_Query As New QueryParameterCollection

Installer path issue

Wed, 25 Nov 2009 10:12:19 Z

I just installed V1.2.21023.14 on top of VS2010 beta 2 on windows 7 x64. The file
C:\Program Files (x86)\MSBuild\4.0\Microsoft.Common.targets\ImportAfter\CodeContracts.targets
was installed at the wrong location - it should have been
C:\Program Files (x86)\MSBuild\v4.0\Microsoft.Common.targets\ImportAfter\CodeContracts.targets
Because of this it was impossisble to create projects in VS.
Hope this helps .

Unclear Warning "CodeContracts: requires unproven"

Wed, 25 Nov 2009 03:54:12 Z

Often I see this warning with no explaination as to what requirement isn't proven.

Automatic Non Null Invariant for Initialized readonly Field in C#

Tue, 24 Nov 2009 20:35:13 Z

Hi,

Why isn't there an automatic assumption by CC that initialized readonly fields in C# will never be null?

namespace TestContracts
{
	class Program
	{
		static void Main(string[] args)
		{
		}

		readonly string value = "Hello";

		int Length
		{
			get
			{
				return value.Length;
			}
		}
	}
}

Message 1 CodeContracts: Suggested precondition: Contract.Requires(this.value != null); [file] 15 5 TestContracts
Warning 2 CodeContracts: Possibly calling a method on a null reference 'this.value' [file] 15 5 TestContracts
Message 3 CodeContracts: Checked 5 assertions: 4 correct 1 unknown [program] 1 1 TestContracts

I understand that even readonly fields can be mutated via reflection, but I don't think that possibility should apply for CC static checking. After all, even if I explicitly specify an object invariant to silence the static checker, the field could still be set to null by reflection at runtime, which means that the invariant is no longer true and all of the checking performed against it at compile time may be invalid at runtime.

Or is there some other subtle technical reason perhaps?

Thanks,
Dave

http://davesexton.com/blog

Inferring invariants

Tue, 24 Nov 2009 19:53:28 Z

I tried to switch on inferring ensures and requires for internal (non-public) methods. This greatly reduces amount code required to pass the static checking. And much more code could be cleaned if we had an option to infer invariants, at least for readonly fields, which are assigned in one place only (in ctor):

class Example
{
readonly int propA;
readonly int[] items;

public Example(int a, int count)
{
     Contract.Requires(a >= 0);
     Contract.Requires(count >= 0);

     this.propA = a;
     this.items = new int[count];
}

[ContractInvariantMethod]
  void Invariant()
{
     // usually many of the statements here could be simply inferred from ctor
     // but we have to write them explicitly. And many of them unnecessarily
     // reevaluated at each public method call (if we enable runtime checking)

     Contract.Invariant(this.propA >= 0); // can be inferred from ctor, never changes during object lifetime
     Contract.Invariant(this.items != null); // can be inferred from ctor, never changes during object lifetime
     ....
}
}

Possible bug?

Mon, 23 Nov 2009 14:18:33 Z

I have found a possible bug in the static checker.

I have two functions A and B with the following postconditions:

public float A()
{
Contract.Ensures(Contract.Result<float>() >= 0);
...
}

public float B()
{
Contract.Ensures(Contract.Result<float>() > 0);
...
}

and a function C with the following precondition:

public void C(float param)
{
Contract.Requires(param >= 0);
...
}

I'm calling C with

C(A() * B());

As A guarantees a result >= 0 and B guarantees > 0, I would expect A*B to be >= 0. However, the static checker complains that C's precondition is not met.

However, if I change the B postcondition to be Contract.Ensures(Contract.Result<float>() > 0), it works.

Is it fixed in latest release about 'Call to impure method in a pure region in method'

Tue, 24 Nov 2009 12:45:31 Z

I got the same error information in my app.

I made some code like

public static bool Update(IClub club)
{
     Contract.Requires(club != null, ClubMessages.Required);
     Contract.Requires(MyDomain.Clubs().Any(i => i.Number == club.Number), ClubMessages.NotExists);
            
     return MyDomain.DataContext().Update(club);
}

An warning will be thrown when it's building.

Detected call to impure method 'System.Linq.Expressions.Expression.Field(System.Linq.Expressions.Expression,System.Reflection.FieldInfo)' in a pure region in method 'MyDomain.AddClub(MyProject.BusinessModels.IClub)'.

I try to refactor the assertion to a separated method as a basic query.

 public static bool IsExists(this IClub club)
 {
     Contract.Requires(club != null,ClubMessages.Required);
     return MyDomain.Clubs().Any(i => i.Number == club.Number);
 }

 public static bool Update(IClub club)
 {
      Contract.Requires(club != null, ClubMessages.Required);
      Contract.Requires(club.IsExists(), ClubMessages.NotExists);
            
       return MyDomain.DataContext().Update(club);
 }

But the warning is still there. it says

Detected call to impure method 'MyProject.BusinessModels.MyDomain.IsExists(MyProject.BusinessModels.IClub)' in a pure region in method 'MyProject.BusinessModels.MyDomain.Update(MyProject.BusinessModels.IClub)'

searched it in google, and got the post

Call to impure method in a pure region in method

It says it's a known issue, and will be fixed in new release.

But i still get the same warning information under vs2010 b2 and Code Contracts 1.2.21023.14.

Anybody can give me some information about it?

Thanks at advance.

Is the contract for stream.read incorrect?

Mon, 23 Nov 2009 05:14:27 Z

The contract for Stream.Read in MSCorLib.Contracts contains the following contract: (via reflector)

    Contract.Requires((bool) ((offset + count) < buffer.Length), null, "offset + count < buffer.Length");

this excludes the following (legal code)
   var buffer = new byte[10];
   var s = /* some stream */
   s.Read(buffer, 0, 10);

This appears to be a bug, I believe the contract (and several related contracts in that same class including beginread and write) should read:
    Contract.Requires((bool) ((offset + count) <= buffer.Length), null, "offset + count < buffer.Length");

Thanks

John Melville

BinaryFormatter Deserialize Missing Ensures Return Not Null

Tue, 24 Nov 2009 11:03:10 Z

Hi,

Could the BinaryFormatter.Deserialize method have a contract that ensures the return value will never be null?

Thanks,
Dave

http://davesexton.com/blog

Contract.ForAll Static Checking

Tue, 24 Nov 2009 10:53:24 Z

Hi,

Any word yet on the status of supporting Contract.ForAll in the static checker?

I'm experiencing the same issue as in the following post using the types built-in to Beta 2.

http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/94ec2bce-61b5-463c-a1b6-22c22a42e67f

Thanks,
Dave

http://davesexton.com/blog

Suggested precondition for null check ignores existing precondition for String.IsNullOrWhiteSpace

Tue, 24 Nov 2009 10:21:32 Z

Hi,

CC seems to ignore the fact that String.IsNullOrWhiteSpace checks for null, yet the same fact for String.IsNullOrEmpty is not ignored.

For example, the following code:

using System.Diagnostics.Contracts;

namespace TestContracts
{
	class Program
	{
		static void Main(string[] args)
		{
			CallFoo("text", "text2");
		}

		static void CallFoo(string text, string text2)
		{
			Contract.Requires(!string.IsNullOrEmpty(text));
			Contract.Requires(!string.IsNullOrWhiteSpace(text2));

			Foo(text);
			Foo(text2);
		}

		static void Foo(string text)
		{
			Contract.Requires(text != null);
		}
	}
}

Produces the following warnings with static checking enabled:

Message 1 CodeContracts: Suggested precondition: Contract.Requires(text2 != null); [file] 17 4 TestContracts
Warning 2 CodeContracts: requires unproven [file] 9 4 TestContracts
Warning 3   + location related to previous warning [file] 15 4 TestContracts
Warning 4 CodeContracts: requires unproven [file] 18 4 TestContracts
Warning 5   + location related to previous warning [file] 23 4 TestContracts
Message 6 CodeContracts: Checked 6 assertions: 4 correct 2 unknown  [program] 1 1 TestContracts

Am I correct in expecting that there should be no suggestions or warnings at all for this program?

Thanks,
Dave

http://davesexton.com/blog

Missing Requires in indexer of ReadOnlyCollection

Wed, 18 Nov 2009 18:43:36 Z

class MyCollection : ReadOnlyCollection<object>
{
public MyCollection()
       : base(new object[0])
   {
   }

   public object GetItem()
   {
       return this[-1];
    }
}

CodeContracts: Checked 1 assertion: 1 correct

Can this be used with the Compact Framework?

Sun, 15 Nov 2009 19:28:00 Z

Will code contracts work on Windows CE running the Compact 3.5 Framework?

Thanks in advance

Suggestion: Contract.Requires(bool condition, Func messageGenerator)

Sat, 21 Nov 2009 01:21:07 Z

Reason: you might not want the message to be evaluated in all error free cases. It might be expensive.

Contract Request by Usage - This method's contracts should be verifiably correct

Fri, 20 Nov 2009 18:11:57 Z

I have the following, relatively complicated, method to split text into lines less than a maximum size:

    <Pure()>
    Public Function SplitText(ByVal body As String, ByVal maxLineLength As Integer) As IList(Of String)
        Contract.Requires(body IsNot Nothing)
        Contract.Requires(maxLineLength > 0)
        Contract.Ensures(Contract.Result(Of IList(Of String))() IsNot Nothing)
        Contract.Ensures(Contract.Result(Of IList(Of String))().Count > 0)

        Dim result = New List(Of String)()
        For Each line In Microsoft.VisualBasic.Split(body, Delimiter:=Environment.NewLine)
            If line.Length <= maxLineLength Then
                result.Add(line)
                Continue For
            End If

            Dim subline = New System.Text.StringBuilder(capacity:=maxLineLength)
            Contract.Assert(subline.Length = 0)
            For Each word In line.Split(" "c)
                Contract.Assert(subline.Length <= maxLineLength)
                If word.Length > maxLineLength Then 'word won't fit on its own line; jam it in!
                    'dump current line
                    If subline.Length > 0 Then
                        Dim n = maxLineLength - subline.Length - 1
                        If n > 0 Then
                            subline.Append(" ")
                            subline.Append(word.Substring(0, n))
                            word = word.Substring(n)
                        End If
                        result.Add(subline.ToString)
                        subline.Clear()
                    End If
                    Contract.Assert(subline.Length = 0)
                    'dump full lines worth of the word
                    Dim p = 0
                    For p = 0 To word.Length - 1 - maxLineLength Step maxLineLength
                        Contract.Assert(p + maxLineLength <= word.Length)
                        result.Add(word.Substring(p, maxLineLength))
                    Next p
                    'continue with remaining portion of the word
                    word = word.Substring(p)
                    Contract.Assert(word.Length <= maxLineLength)
                    Contract.Assert(subline.Length = 0)
                ElseIf subline.Length = 0 Then 'first word on new line
                    'no action needed, we already know the word will fit
                ElseIf subline.Length + 1 + word.Length <= maxLineLength Then 'word will fit
                    subline.Append(" ") 'separate from previous word
                Else 'word won't fit on current line, start new line
                    result.Add(subline.ToString)
                    subline.Clear()
                End If

                Contract.Assert(subline.Length + word.Length <= maxLineLength)
                subline.Append(word)
                Contract.Assert(subline.Length <= maxLineLength)
            Next word
            Contract.Assert(result.Count > 0 OrElse subline.Length > 0)

            'Dump last line
            If subline.Length > 0 Then
                result.Add(subline.ToString)
            End If
            Contract.Assert(result.Count > 0)
        Next line
        Return result
    End Function

Contracts 1.2.21023.14 gives the following warnings:
- Couldn't prove result.count > 0 [probably because there are no contracts on the vb variant of the Split function]
- Couldn't prove a bunch of assertions involving subline.length [probably there are no, or not enough, contracts on Text.StringBuilder]
- Couldn't prove word.length <= maxLineLength [probably because the verifier doesn't understand the for-loop well enough]

Static checker fails to identify obvious problems

Fri, 13 Nov 2009 12:47:52 Z

Hi,
I'm currently experimenting code contract, so I wrote this very simple piece of code:

    public class Test
    {
        private List<int> list;

        public Test()
        {
            list = new List<int>();
        }

        public List<int> List
        {
            get { return list; }
        }

        [ContractInvariantMethod]
        protected void ObjectInvariant()
        {
            Contract.Invariant(list.Count == 0);
        }
    }

The static checker doesn't see any problem with that code, although I can obviously do that and break the invariant:

Test t = new Test();
t.List.Add(1);

Can someone shed some light on that?

Thanks

More trouble with mixed-mode projects

Thu, 19 Nov 2009 15:15:50 Z

I have a C# project that references a mixed-mode C++/CLI assembly in the same solution. When I'm enabling static checking on this, I'm getting the following warning:

Warning 71 Contract reference assembly for project 'MyMixedModeProject' not found. Select 'Build' or 'DoNotBuild' for Contract Reference in project settings. MyManagedProject

How can I get rid of this warning? There is no "code contracts" tab in the mixed mode project. Quite often this causes the static checker to give up.

Contract Requests - Net.IPEndPoint, Net.IPAddress, and a new postcondition for String.IndexOf

Fri, 20 Nov 2009 03:41:51 Z

Please add contracts to Net.IPEndPoint and Net.IPAddress. Eg. GetAddressBytes() != null

String.IndexOf should have the following postcondition:
result == -1 || result <= this.length - value.length

So that, for example, this code will have no warnings on the SubString line:

Public Module M
    Public Function TryGetTail(ByVal value As String, ByVal divider As String) As String
        Contract.Requires(value IsNot Nothing)
        Contract.Requires(divider IsNot Nothing)
        Dim p = value.IndexOf(divider)
        If p = -1 Then Return Nothing
        Return value.Substring(p + divider.Length)
    End Function
End Module

Rewrite failed to produce verifiable assembly

Tue, 17 Nov 2009 05:04:57 Z

I discovered that if you have runtime checking enabled for a project, and there are no code contracts in it, you will get a compile error "Rewrite failed to produce verifiable assembly". Knowing this now, it's easy to resolve. But it can sometimes take a while to figure this out. It came up because I was writing a tutorial on Code Contracts, and I wanted to start the user with a code base without code contracts, but with contracts enabled so they could focus on the basics.

It's not a big deal, but if you can make it a friendlier experience, it may help reduce frustration for novices. In the meantime, for my exercises, I merely add a dummy class with a code contract, and all is well. I may change that to require them to enable the setting themselves. After all, it is a tutorial.

Best Regards, David K Allen Minneapolis, Minnesota, USA

Setting Runtime Checking in VS 2010 Beta 2 Team

Tue, 17 Nov 2009 16:00:18 Z

I had Code Contracts in place which worked - displaying a dialog on failure.

Today, they do not work. They are simply overlooked even though they should be failing.

I assume that something happened which resulted in runtime checking being turned off.

So, I tried to find where to turn runtime checking back on, and I do not have a Code Contracts tab in any project properties dialog, this project or a new project.

Ideas as to why the tab is missing, a mechanism for retrieving it, guesses as to why runtime checking was turned off (without my involvement), another way to turn runtime checking, or any other thoughts.

One more variation of Assert/Assume

Thu, 19 Nov 2009 11:09:52 Z

Suppose we want to deploy some code dll with runtime checking enabled. Desired checking level == Preconditions.

I would suggest to add one more variant of Assert/Assume (Contract.Verify() for examaple), which will behave exactly like Assume, but will remain in assembly if we compile with checking levels != Full. This is how we might use it:

    void Test()
    {
        int x = CallExternalLib(); // called method has no contracts

        // we only need this Assume to satisfy the static checker,
        // we don't want this check to stay in production dll
        // because the condition will be checked within DoSomething()
        // which has Contract.Requires(x >= 0)

        Contract.Assume(x >= 0);

bool success = DoSomething(x); // requires x >= 0

        // but we want this check to stay in production dll,
        // because the result of DoSomething cannot be statically proven
        Contract.Assume(success);

        // suggested alternaltive (stays in assembly even when checking level != Full)
        // Contract.Verify(success)
    }

Adding ensures causes other contracts to fail

Sun, 08 Nov 2009 04:35:35 Z

Ok, I have the following:

        [Pure]
        public override string NodeName
        {
            get
            {
                return "#comment";
            }
        }

All my contracts are proven by the static checker. However, when I change it to this:

        [Pure]
        public override string NodeName
        {
            get
            {
                Contract.Ensures(Contract.Result<string>() == "#comment");

                return "#comment";
            }
        }

I get other (apparently unrelated) contracts failing. The point of failure is the 'return' line.

The contracts in question are on the superclass of this, in an invariant:

        [ContractInvariantMethod]
        protected new void ObjectInvariant()
        {
            Contract.Invariant(dataField != null);
            Contract.Invariant(TextContent == dataField); // fails
            Contract.Invariant(NodeValue == dataField); // fails
            Contract.Invariant(Data == dataField);
        }

Is this a bug in Contracts, or am I doing something wrong?

I can supply full source if that will help.

Default Display Hides Abort/Retry/Ignore Buttons

Tue, 17 Nov 2009 17:13:10 Z

Hopefully this is fixed in current builds, but in my beta 2 on my contracts that come from a WPF app the stack is very large. The critical Abort/Retry/Ignore buttons are off the bottom of the screen. Also, the red x to close is disabled. I'm really hoping this is already fixed or some part of the following can make the bar to fix:

- Provide a scrolling region to ensure the buttons are always visible at the bottom and the stack is still visible
- Move the buttons to the top and allow us to debug and use a call stack window trace if we need that info
- Enable the Red X to close as Abort or Retry. ANYTHING is better than having a window stuck open on the screen

If you have not seen this and need more information, please let me know.

Can't create projects in VS2010 Beta 2 after installing devlabs package

Thu, 12 Nov 2009 07:52:43 Z

I installed the devlabs package to enable the tool support in VS2010 beta 2 and now cannot create projects

The symptom I see is that it says that from C:\program files\msbuild\4.0\microsoft.common.targets\ImportAfter\codecontracts.targets it cannot find
c:\msbuild\4.0\Microsoft.CodeContracts.Targets

This appears to be a problem with CodeContractsInstallDir not being set up properly - anyone know whats going on?

Richard Blewett, thinktecture - http://www.dotnetconsult.co.uk/weblog2
Twitter: richardblewett

Contracts and Constructor Overloading

Mon, 16 Nov 2009 06:00:26 Z

So very late to the party, I know. But I've spent a solid day trying to find the limits of the current drop of Code Contracts, and I was wondering if there was a more optimal way to share contracts between constructors than duplicating identical statements:

For example:


public class Person
{
    private string firstName { get; set; }
    private string lastName { get; set; }
    private int age { get; set; }

    public Person(string firstName, string lastName)
    {
        Contract.Requires(!string.IsNullOrEmpty(firstName)); // <-- "location related to previous warning"
        Contract.Requires(!string.IsNullOrEmpty(lastName));

        this.firstName = firstName;
        this.lastName = lastName;
    }

    public Person(string firstName, string lastName, int age) // <-- "CodeContracts: requires unproven"
        :this(firstName, lastName)
    {
        // the tools return "requires unproven" warning for this constructor
        // with an related warning for the marked line above
        // and suggests adding these Requires
       
        // Contract.Requires(!string.IsNullOrEmpty(firstName));
        // Contract.Requires(!string.IsNullOrEmpty(lastName));

        // uncommenting these lines satisfies the tools

        Contract.Requires(age > 0);
        this.age = age;
     }
     // ...more code
}

I'm assuming that the requirements in the first constructor would be applied to the second constructor - is this a limitation of the current tools, or have I overlooked something?

Problem with Contracts affecting other objects

Sat, 14 Nov 2009 09:16:17 Z

Hello,

let's take the following class:

public sealed class Foo
{
    public bool IsOpen
    {
        get;
        private set;
    }

    public IDisposable Open()
    {
        Contract.Ensures(this.IsOpen);

        this.IsOpen = true;

        return new Disposer(() => this.IsOpen = false);
    }
}

with that helper class

public sealed class Disposer
    : IDisposable
{
    private readonly Action _action;

    private Action Action
    {
        get
        {
            Contract.Ensures(Contract.Result<Action>() != null);

            return this._action;
        }
    }

    public Disposer(Action action)
    {
        Contract.Requires(action != null);

        this._action = action;
    }

    public void Dispose()
    {
        this.Action();
    }
}

Now I am writing code like the following:

Foo foo = new Foo();

using (foo.Open())
{
    Contract.Assert(foo.IsOpen);
}

Contract.Assert(!foo.IsOpen);

How can I prove the last assert?

There should be a possibility to modulate Contracts affecting other objects.

Cheers
winSharp93

What is the purpose of ContractPublicPropertyName attribute?

Tue, 03 Nov 2009 08:19:22 Z

Still unclear to me. If there is a public property which correponds to a private field, why can't we just use that public property instead of the private field where we need to satisfy the visibilty rules?

Unexpected BadImageFormatException in a GroupBy poscondition using CodeContract in VS2010 Beta1

Fri, 09 Oct 2009 04:52:27 Z

The attempt to run a custom GroupBy with the second of the following contract poscondition produces an unexpected bad image format error

static class ContractedQueryMethods {

public static IEnumerable<IGrouping<K, T>> GroupBy<T, K>(this IEnumerable<T> source,

Func<T, K> selector) {

//This poscondition is correctly verified in runtime

Contract.Ensures(Contract.Result<IEnumerable<IGrouping<K, T>>>().

Select(x => x.Count()).Sum() == source.Count(),

"The total items of all groups is equal to the total items in the source");

//The following poscondition produces an unexpected error during injection of the code!

Contract.Ensures(Contract.ForAll<T>(

source,

(x => Contract.Result<IEnumerable<IGrouping<K, T>>>().Any(y => y.Contains(x)))),

"Each item from the source belongs to some group");

//...

return Enumerable.GroupBy(source, selector);

}

//...

}

Message:

BadImageFormatException was unhandled

An attempt was made to load a program with an incorrect format (Exceptipn from HRESULT: 0x80070008

Contract Information API (Reflection like)?

Wed, 11 Nov 2009 20:05:38 Z

Hello,

are there any libraries available for getting contract information out of the Contract Assemblies?

Although it is not that important, it would be to have a "reflection-like" API for this purpose.

Its usage could look like that schematically:

MemberInfo member = //...
ContractInformation info = ContractInformation.ForMember(member);

foreach (Precondition precondition in info.Preconditions)
    Console.WriteLine(precondition.Condition);

This would complete the existing reflection APIs.

Cheers
winSharp93

CodeContracts XML docs not getting generated

Thu, 05 Nov 2009 21:55:32 Z

There were reports that the XML contract generation was not working and indeed it ins't in the latest release due to a refactoring bug in the build scripts.

If you want to fix it yourself, here's what to change:

You need to edit both of the following files (need Admin privilege)

%Program Files%\Microsoft\Contracts\MsBuild\v3.5\Microsoft.CodeContracts.targets

%Program Files%\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets

Find the section below and make the Condition match the highlighted text.

<!--=====================================================================

Add post build step for contract XML documentation generation

======================================================================-->

<PropertyGroup

Condition="'$(CodeContractsEmitXMLDocs)' == 'true'">

<PrepareForRunDependsOn>$(PrepareForRunDependsOn);ContractXmlDocumentation</PrepareForRunDependsOn>

</PropertyGroup>

The erroneous version looks like this:

<!--=====================================================================

Add post build step for contract XML documentation generation

======================================================================-->

<PropertyGroup

Condition="'$(CodeContractsEmitXMLDocs)' == 'true' and '$(CodeContractsBuildReferenceAssembly)' == 'true'">

<PrepareForRunDependsOn>$(PrepareForRunDependsOn);ContractXmlDocumentation</PrepareForRunDependsOn>

</PropertyGroup>

Cheers, -MaF (Manuel Fahndrich)

Team System only?

Tue, 24 Feb 2009 04:38:34 Z

My organization doesn't use Team System, we use Professional Edition. I don't understand why the "academic version" works with any version, but the "commercial version" (which is what we would have to have in order to use Code Contracts in our applications) requires Team System. Is this yet another way to try to force people into buying a more expensive SKU that they don't need?

Moderator | MCTS .NET 2.0 Web Applications | My Blog: http://www.commongenius.com

Missing invariant, bad(?) invariant, and an odd warning

Thu, 12 Nov 2009 20:55:54 Z

hello,

I've been playing with CodeContracts, and it's very cool. I'm experimenting with it on a fairly large codebase. some requests and a question:

please add a Count == Length invariant to BitArray. that's correct per the documentation, and would clean up a heap of warnings for me. Stream.Read()'s postcondition that has already been mentioned before is biting me too (should be offset + count <= buflen instead of <).

also, ICollection.Add seems to have a "count == oldCount + 1" postcondition on it. the documentation says nothing of this, and for my (pre-4.0) set implementation it isn't true, so this now throws up at runtime. can it be "count == oldCount || count == oldCount + 1" or something?

and I'm puzzled about a generated warning. consider:

    class Program {
        static void Foo(List<byte[]> fs) {
            Contract.Requires(fs != null);
            Contract.Requires(fs.Count > 0);
            Contract.Requires(Contract.ForAll(fs, f => f != null));
            int l = fs[0].Length;
        }
    }

this pops an "Possible use of a null array" on the last line, right after the Require() that should tell it none of them are null. am I missing something?

also, is there a better venue to post these kinds of things than this forum? something like a bugzilla?

thank you,
Lodewijk

Requires unproven: value != -2147483648

Wed, 11 Nov 2009 16:01:33 Z

The static verifier seems to randomly display this warning that "requires unproven: value != -2147483648". I encounter this warning three times in my code base, for example here

for (int i = 0; i < combo.MultisampleCounts.Count; i++)
{
    int type = combo.MultisampleCounts[i];

    Contract.Assume(combo.MultisampleQualities.Count > 0);

    int quality = combo.MultisampleQualities[0];

    if (Math.Abs(type - input.SwapChainDescription.SampleDescription.Count) < Math.Abs(bestCount -
        input.SwapChainDescription.SampleDescription.Count))
    {
        bestCount = type;
        bestQuality = Math.Min(quality - 1, input.SwapChainDescription.SampleDescription.Quality);
    }
}

it warns me of the loop initialization (int i = 0) and also of the condition in the if statement.
Do you have any ideas what is going on?

Precondition failed: offset + count < buffer.Length for Stream.Read method

Sat, 07 Nov 2009 21:39:48 Z

The contract libraries shipped with 1.2.21023.14 have the following Contract.Requires for Stream.Read:

Contract.Requires((bool) ((offset + count) < buffer.Length), null, "offset + count < buffer.Length");

This contract requires should be: offset + count) <= buffer.Length

The same issue applies to other Stream methods.

division checks

Thu, 12 Nov 2009 10:38:44 Z

When I run the static checker on this method, having turned on implicit arithmetic checks,

public int Divide(int x, int y) { return x / y; }

it does complain about y possibly being null.
But Pex also generates the following test case, that shows that an OverflowException is thrown for (int.MinValue, -1):

[TestMethod]
[PexRaisedException(typeof(OverflowException))]
public void Divide03()
{
this.Divide(int.MinValue, -1);
}

Why doesn't the static checker complain about this?

Nikolai Tillmann - Tell us how you use Pex

Contracts and reflection

Wed, 11 Nov 2009 14:22:57 Z

When I verify contracts on this code

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.ComponentModel;
using System.Diagnostics.Contracts;

namespace ContractTest
{
    public sealed class MyClass
    {
        public int MyProperty { get; set; }

        public void Test()
        {
            Contract.Requires(GetType() != null);
            Contract.Requires(GetType().GetProperties() != null );
            Contract.Requires(GetType().GetProperties().Length == 1);
        }

        public void Test2()
        {
            Test();
        }
    }
}

I get

MyClass.cs(23,13): warning : CodeContracts: requires unproven
MyClass.cs(18,13): warning :   + location related to previous warning

It's complaining about the line

Contract.Requires(GetType().GetProperties().Length == 1);

Am I missing something or is the static checker unable to verify constraints based on reflection?