1
Vote

Unsoundness when verifying code with variables declared as static

description

Hello,

The following code is verified in VCC although the assertion clearly does not hold.

include <vcc.h>

void main()
{
stat();
stat();
}

void stat()
{
 static int s=0;
 _(assert s==0)
 s=1;
}

Verification of main succeeded. [1.19]

Verification of stat succeeded. [0.00]

Seemingly, VCC treats variable s as a non-static local variable instead of a static local variable.
Does anyone have an idea why this is the case? Is this issue simply a bug or does it extend to a conceptual flaw?

/Jonas

comments

erniecohen wrote Mar 13 at 6:29 PM

This is a bug. Static variables are unsupported, so their use should give an error message.

Conceptually, static variables are essentially globals. But unlike globals, they can't be referred to outside of the body of the containing function, so there's no way to mention them in contracts. So to support them, we would have to give them a name outside the function, which more or less defeats the purpose in using them in the first place.