Object Initialization

Mar 8, 2010 at 4:20 PM

Hello all, I have a quick question relating the writes() clauses when an object has not been initialized and is not expected to be wrapped (during an initilization function). Like:

typedef struct _s {
	unsigned int a, b;
	invariant ((a+b) < 300)
} S, *SP;

void init(SP s)
	s->a = 0;
	s->b = 1;

Verification of this little example fails with the message:

Assertion 's->a is writable' did not verify.

other functions like:

void swap(SP s)
	unsigned int temp;
	temp = s->a;

verify without problems.

The question would be: How do I specify that function "init" may write to the structure even when it hasn't been initalized?


Thanks a lot in advance folks,


Mar 8, 2010 at 4:43 PM
Edited Mar 8, 2010 at 4:53 PM

Hi Sergio,

the problem with you first function is that s is not wrapped at function start and so the caller might still have knowledge about s->a and s->b. Thus, writing to these fields requires them (and not only 's') to be in the function's writes clause. So, writing 'writes(s, &s->a, &s->b)' (or equivalently 'writes(span(s))') makes the function verify.

You can read more about the reason for this at http://vcc.codeplex.com/wikipage?title=Framing%20and%20freshness, especially "So we check that the thing we’re writing to is mutable and that it was changed to mutable after the beginning of the current function (or it was listed in writes clause)." This also explains why your second function works: there, you unwrap s after the beginning of the function.


Hope that helps!


Mar 8, 2010 at 4:45 PM
Edited Mar 8, 2010 at 4:47 PM

This is only my amateur take on this issue, so please wait for an expert to confirm exactly what is going on before you cite me on this. I hope my naive point of view helps :)

In the first example, you need to specify exactly what fields of s are written in by your function. In this case, since you write in all fields, you would replace your "writes(s)" contract by a "writes(span(s))". Writing in the structure does not necessarily mean writing in its fields...

The second example goes through because the unwrapping immediately makes the whole structure's span writable.


Edit: The expert confirmed a few seconds before I posted.

Mar 8, 2010 at 4:49 PM

Wow that was quick, thank you very much guys. It definitely helped a lot.