This project is read-only.

Missing writes check when unwrapping struct with 'dynamic_owns'

Jun 30, 2011 at 1:45 PM

Hi all,

according to the VCC tutorial, _(unwrapping a) { ...} is a shorthand for _unwrap(a) ... _wrap(a).

However, in the example below, unwrapping a struct marked with "dynamic owns" is possible without mentioning a writes clause in the method contract. 

Using unwrap/wrap explicitely works as intended:

>vcc /version
Microsoft Research Vcc Version 2.1.40630.0
Microsoft Research Boogie Version 2.1.30608.1
Microsoft Research Z3 Version 2.0.41203.1

> vcc /2
[...] error VC8510: Assertion 'a is writable in call to unwrap a' did not verify.

Comparing the Boogie output of both versions shows that when using "unwrapping", no writes_check is generated. Using unwrap/wrap, the Boogie code includes:

// assert @writes_check(a);  
assert $top_writable($s, #wrTime$1^5.1, $ptr(^S, P#a));

Is this a bug or is the definition of unwrapping in the tutorial missing something?

Thanks,

Thorsten


#include "vcc.h"

_(dynamic_owns) struct S { int i; };

void test(struct S *a)
  _(requires \wrapped(a))
{ 
	_(unwrapping a) { 
		a->i = 0; 
	} 
}
Jun 30, 2011 at 2:12 PM

This is a bug.

I've copied it into a work item...

Thanks!

Mark

Jun 30, 2011 at 2:12 PM
This discussion has been copied to a work item. Click here to go to the work item and continue the discussion.
Jun 30, 2011 at 2:17 PM

Thanks for confirming this issue.

Best,

Thorsten

Jul 28, 2011 at 10:27 AM

I have just checked in a fix for this issue.

Stephan