constructedtypemethodcontractsnotresolvedbug

Cancel Edit [WikiEntry.PreviewButtonText] Save
Summary: A call of a method of a constructed type causes the Spec# Program Verifier to crash if the method has a contract and the contract contains things that need to be resolved, such as qualified identifiers.

Nearby: KnownBugsOrProblems, HomePage

Reproduced on: December 2005 release (1.0.5612)

The following program causes Boogie to crash:

		 class Account
		 {
		     public int Balance;
		 }
		 class Cell<T>
		 {
		     public void Foo(Account/*!*/ account)
		     //^ requires 0 < account.Balance;
		     {
		     }
		 }
		 static class Program
		 {
		     static void Main()
		     {
		         Cell<object> cell = new Cell<object>();
		         Account account = new Account();
		         cell.Foo(account);
		     }
		 }
Cancel Edit [WikiEntry.PreviewButtonText] Save
Microsoft Communities