how to use write clause when a function will be called more than once

Jun 1, 2011 at 3:42 PM

struct GS
{
	int a;
};

struct GS g;

void f1(int x)
	ensures(g.a == x)
	writes(span(&g))
{
	g.a = x;
}

void f2()
	writes(span(&g))
{
	f1(0);
	f1(1);
	f1(2);
}

The VCC reports that "Error    1    Assertion '_vcc_span(&g) is writable in call to f1(1)' did not verify.   "

"Error    2    Assertion '_vcc_span(&g) is writable in call to f1(2)' did not verify.   "

If I just call "f1" once in function "f2", then VCC will report success.

Editor
Jun 1, 2011 at 3:51 PM

The problem here is that, by giving f1 the right to write g's span, you also technically allow it to wrap g, or do other nasty things to it, making it unwritable by subsequent calls. The best solution in your case would be to add a postcondition to f1, as follows.

void f1(int x)
	ensures(g.a == x)
	writes(span(&g))
        ensures(mutable(&g))�
{
	g.a = x;
}

Disclaimer: I haven't taken the time to test this, so I have no idea if it actually works. You may have to play with combinations of mutable and span(&g), and also make sure that g's embedding is not modified... If it works as described, kudos to me :)

Hope this helps. Cheers,
Francois 

Jun 1, 2011 at 5:08 PM

Thank you! It works!

Jun 2, 2011 at 1:02 AM
Edited Jun 2, 2011 at 1:20 AM

 

struct GS
{
	int a;
	int b;
};

struct GS ga[4];

void write_fun(int idx)
	writes(span(&ga[idx]))
ensures(mutable(&ga[idx]))
 { ga[idx].a = 0; ga[idx].b = 0; } void call_write(void) writes(array_range(ga, 4)) { int i; for (i = 0;i < 4; i++) { assume(i >= 0 && i < 4); write_fun(i); } }

 

The VCC reports that "Error    1    Assertion '_vcc_span(&ga[idx]) is writable in call to write_fun(i)' did not verify.   "

When I unroll the loop in function "call_write" like this: 

 

void call_write(void)
	writes(array_range(ga, 4))
{
	write_fun(0);
	write_fun(1);
	write_fun(2);
	write_fun(3);
}

 

The VCC reports success.

Why?

Editor
Jun 7, 2011 at 9:18 PM

You need to give an invariant to the loop, as VCC cannot infer it by itself. I think in this case you are going to need something like the following (you may have to adapt, as I don't have VCC running on this machine and can't test).

for (i = 0; i< 5; i++)
invariant(0 <= i && i < 5)
invariant(forall int j; 0 <= j && j < 5 ==> mutable(ga + j))
{
...
}

Cheers,
Francois