This project is read-only.

Impure method call to committed object verifies

Jul 25, 2010 at 7:23 PM
Edited Jul 25, 2010 at 7:25 PM

Hi,

the following code contains a call to an impure method of a committed object in the line marked with (*). Still, this code verifies. I don't understand why as calls to impure methods are allowed for consistent targets only.

Regards,

Boris

 

using System;

using Microsoft.Contracts;





public class A

{

	int a;

	

	public void f(int m)

	{

		a = m;

	}

}







public class B

{

	[Pure] public int g()

	{

		return 0;

	}

}







public class C 

{

	[Rep] public A a = new A();

	[Rep] public B b = new B();	

}





	

public class D

{

	[Rep] public C c = new C();



	public void f() {

		int m;

		

		m = c.b.g();

		c.a.f(m);  // (*) 
	}

}

Jul 26, 2010 at 1:31 PM
Hi Boris, You ran into a bug in the Spec# verifier. The variation of your code below illustrates the bug. I am working on the fix and will commit it soon (I believe I have fixed it, but I am having trouble accessing the sources on CodePlex). Peter using System; using Microsoft.Contracts; public class B { [Pure] public int g() { return 0; } } public class C { [Rep] public B b = new B(); } public class D { [Rep] public C c = new C(); public void f() { int m; m = c.b.g(); assert false; // verifies } }
Jul 26, 2010 at 4:35 PM
Hello Peter, I encounter this problem with the Spec# release for VS 2008 that was previously available on the CodePlex site. I've seen there's a new version from last week (change set 55325) which I haven't tested. Is this bug also present in this version? Regards, Boris
Jul 26, 2010 at 5:12 PM
Hi Boris, I work with the source distribution. As I said, I am having problems with the svn access. But I believe my sources are up to date, and there is defninitely a bug there. Cheers, Peter
Oct 12, 2010 at 9:09 AM

Hello Peter, any news on this? Boris

Oct 12, 2010 at 12:00 PM

Hi Boris, I fixed the problem, but currently I cannot build sscboogie because the Boogie source has been parted to C#, which breaks the sscboogie build. We are working on changing the sscboogie code, and as soon as I can build again, I will test and commit my fix for your problem. Sorry about the delay! Peter

Nov 10, 2010 at 12:01 PM

Hi Boris,

I was finally able to test and upload my fix for your bug. Sorry this has taken so long! The bugfix is already in the source repository. Tomorrow you should be able to download the nightly build of Nov 11, which will then include the fix. To do that, go to Downloads, click on "Planned" next to "Other Downloads" on the right-hand side of the page. Then click on "Nightly builds" below and download the latest one (it should have "2010-11-11" in the file name).

   Peter