locked
Bug: Warning SR10(0x0) RRS feed

  • Question

  • Hi,

    I'm getting unexpected and strange warnings for the code posted below.  Is this a bug in the static checker?

    Static checker warnings:

    Warning 2 + location related to previous warning	[file]	43	5
    Warning 3 + SR10[0x0]: location related to previous warning		1	1
    Message 4 CodeContracts: Checked 19 assertions: 18 correct 1 unknown	[program]	1	1
    Warning 1 CodeContracts: ensures unproven: Initialized	[file]	71	5

    What is, "Warning 3 + SR10[0x0]"?  There is no "previous warning".

    I expected no warnings at all.  It seems that I've provided enough information for the static checker to prove all contracts.  Am I missing something?

    Code: (VS 2010, .NET 4.0)

    namespace TestContracts
    {
    	class Program
    	{
    		static void Main()
    		{
    			object value = GetValue(new Foo());
    		}
    
    		static object GetValue(Foo foo)
    		{
    			Contract.Requires(foo != null);
    			Contract.Ensures(foo.Initialized);
    
    			return foo.Value;
    		}
    	}
    
    	[ContractClass(typeof(IFooContract))]
    	interface IFoo
    	{
    		bool Initialized { get; }
    		object Value { get; }
    	}
    
    	[ContractClassFor(typeof(IFoo))]
    	abstract class IFooContract : IFoo
    	{
    		public bool Initialized { get { return false; } }
    		public object Value
    		{
    			get
    			{
    				Contract.Ensures(Initialized);
    				return null;
    			}
    		}
    	}
    
    	class Foo : IFoo
    	{
    		public bool Initialized
    		{
    			get
    			{
    				Contract.Ensures(Contract.Result<bool>() == (value != null));
    
    				return value != null;
    			}
    		}
    
    		private object value;
    		public object Value
    		{
    			get
    			{
    				Contract.Ensures(value != null);
    
    				if (value == null)
    					value = new object();
    
    				// ensures unproven: Initialized
    				return value;
    			}
    		}
    	}
    }

    Thanks,
    Dave


    http://davesexton.com/blog
    Saturday, June 26, 2010 4:42 PM

Answers

  • Hi Dave,

      you can use "-show progress -sortwarns=false" which will report in the output window the methods as they are analyzed and avoids sorting warnings, and immediately report them.

    Feel free to send a repro directly to me!

    Thanks,

    f

     

     

     

    • Marked as answer by Dave Sexton Thursday, August 5, 2010 2:11 PM
    Thursday, August 5, 2010 5:22 AM

All replies

  • Hi,

    I've found more strange warnings related to the previous code.  Here's a class that composites two IFoo instances and also implements IFoo itself.

    Additional static checker warnings:

    Warning 4 CodeContracts: ensures unproven: Contract.Result<bool>() == first.Initialized && second.Initialized	[file]	36	9
    Warning 6 CodeContracts: ensures unproven: Contract.Result<bool>() == first.Initialized && second.Initialized	[file]	36	9
    Warning 8 CodeContracts: ensures unproven: Initialized	[file]	44	9

    Warnings 4 and 6 are duplicates.  Furthermore, it seems strange that the static checker cannot prove any contracts on the new class.

    Additional code: (VS 2010, .NET 4.0)

    class CompositeFoo : IFoo
    {
    	public bool Initialized
    	{
    		get
    		{
    			Contract.Ensures(Contract.Result<bool>() == first.Initialized && second.Initialized);
    
    			// ensures unproven: Contract.Result<bool>() == first.Initialized && second.Initialized
    			return first.Initialized && second.Initialized;
    		}
    	}
    
    	public object Value
    	{
    		get
    		{
    			var unused = second.Value;
    
    			Contract.Assert(second.Initialized);
    
    			// ensures unproven: Initialized
    			return first.Value;
    		}
    	}
    
    	private readonly Foo first = new Foo();
    	private readonly Foo second = new Foo();
    
    	[ContractInvariantMethod]
    	void ObjectInvariant()
    	{
    		Contract.Invariant(first != null);
    		Contract.Invariant(second != null);
    	}
    }

    Thanks,
    Dave


    http://davesexton.com/blog
    Saturday, June 26, 2010 5:13 PM
  • Hi,

    Is the problem that the static checker assumes all property getters are side-effect free, so it's tripping up over my lazy implementation?  If so, are there any plans to support lazy initialization in property getters?

    Thanks,
    Dave


    http://davesexton.com/blog
    Saturday, June 26, 2010 5:28 PM
  • Hi,

    I'm not sure about the contracts, but in

     

    Contract.Ensures(Contract.Result<bool>() == first.Initialized && second.Initialized);

     

    the equality operator is of higher precedence than conditional and, so your expression would be equivalent to

    Contract.Ensures((Contract.Result<bool>() == first.Initialized) && second.Initialized);

    Sunday, June 27, 2010 12:50 PM
  • Hi,

    Thanks, you're right about that.  I simply forgot to add parenthesis.  So that leaves the question of why can't the ensures be proven on CompositeFoo.Value, as well as my original questions.

    Thanks,
    Dave


    http://davesexton.com/blog
    Sunday, June 27, 2010 5:55 PM
  • Hi Dave,

      I've tried the first version with my latest snapshot, and it passes the checker with no warnings. So I think we already fixed it. Is it showing up also with the last version?

    Thanks,

    f

    • Proposed as answer by Francesco Logozzo Wednesday, July 21, 2010 12:02 AM
    • Marked as answer by Dave Sexton Wednesday, August 4, 2010 11:59 AM
    • Unmarked as answer by Dave Sexton Wednesday, August 4, 2010 12:15 PM
    Wednesday, July 21, 2010 12:02 AM
  • Hi,

    Yes, it appears to have been fixed in the latest release.  Thanks.

    - Dave


    http://davesexton.com/blog
    Wednesday, August 4, 2010 12:00 PM
  • Hi,

    Sorry but I made a mistake; it appears that something was fixed, although I'm getting a different warning now in my real codebase (I haven't tried a simplified repro yet):

    (1,1): warning : + SR27[0x0]: location related to previous warning
    (1,1): warning : + SR53[0x0]: location related to previous warning

    Is there a static checker switch that I can use to narrow down the scope of the issue?

    Thanks,
    Dave


    http://davesexton.com/blog
    Wednesday, August 4, 2010 12:20 PM
  • Hi Dave,

      you can use "-show progress -sortwarns=false" which will report in the output window the methods as they are analyzed and avoids sorting warnings, and immediately report them.

    Feel free to send a repro directly to me!

    Thanks,

    f

     

     

     

    • Marked as answer by Dave Sexton Thursday, August 5, 2010 2:11 PM
    Thursday, August 5, 2010 5:22 AM