Apr 19, 2010 at 11:27 AM
Edited Apr 19, 2010 at 11:38 AM

Hello all,
I am new to this project and have some low level questions about verification and its usage. I am really confused and would like to know: (1) how to verify a returning value from function which returns a local variable or a result from another function and
(2) how do I declare local variables as mutable. The same with pointers. (3) Is there a way to verify an incremented pointer like p+=32?
Another one lies somewhere between theory and practice.
(4) What does the error 'is typed' in vcc exactly mean?
I provided below an example with all my current issues in it. First functionA() is ok.static void functionA( unsigned int out[32], const unsigned int a[32], const unsigned int b[32])
writes(array_range(out, 32))
reads(array_range(a, 32))
reads(array_range(b, 32))
requires(is_mutable_array(out, 32))
requires(is_thread_local_array(out, 32))
requires(is_thread_local_array(a, 32))
requires(is_thread_local_array(b, 32))
requires(set_disjoint(array_range(a,32), array_range(b,32)))
requires(set_disjoint(array_range(out,32), array_range(a,32)))
requires(set_disjoint(array_range(out,32), array_range(b,32)))
{
unsigned int i;
for(i=0; i<31; i++)
invariant(0<=i && i<=31)
invariant(forall (unsigned int k; 0<=k && k<i ==> out[k] == (a[k] ^ b[k])))
{
out[i] = a[i] ^ b[i];
assert(out[i] == (a[i] ^ b[i]));
}
out[31] = 0;
assert(out[31] == 0);
}
/*
vcc : Verification of functionA succeeded. [0,67]
Time: 1,09s total, 0,42s compiler, 0,00s Boogie, 0,67s method verification.
*/
static unsigned int FunctionB( unsigned int *c, unsigned long long clen, const unsigned int *a, const unsigned long long alen)
writes(array_range(c, clen))
reads(array_range(a, alen))
reads(alen)
requires(is_mutable_array(c, clen))
requires(is_thread_local_array(c, clen))
requires(is_thread_local_array(a, alen))
requires(clen >= 64)
requires(alen >= 64)
// Is there a way to verify return value which is a local variable or another function (return functionA(...))?
returns((clen%64)?0:u)
{
unsigned int fBa[64];
unsigned int fBb[64];
unsigned int i;
unsigned int u;
unsigned long long j;
for(i=0; i<64; i++)
invariant(0<=i && i<=64)
invariant(forall (unsigned int k; 0<=k && k<i ==> ((fBa[k] == a[k]) && (fBb[k] == 0))))
{
fBa[i] = a[i];
assert(fBa[i] == a[i]);
fBb[i] = 0;
assert(fBb[i] == 0);
}
while (clen >= 64)
invariant(0 <= clen)
{
/*
Any suggestions how do I declare fBb as mutable?
error VC8510: Assertion '_vcc_array_range(out, 32) is writable in call to functionA(fBb, fBa, a)' did not verify.
error VC9502: Call 'functionA(fBb, fBa, a)' did not verify.
error VC9599: (related information) Precondition: '_vcc_is_mutable_array(out, 32)'.
*/
functionA(fBb, fBa, a);
functionA(fBb+32, fBa+32, a+32);
u = 1;
assert(u == 1);
for (i = 0;i < 64;++i)
invariant(0<=i && i<=64)
{
/*
What does 'is typed' in this context mean?
error VC8506: Assertion 'c[i] is typed' did not verify.
error VC8507: Assertion 'c[i] is writable' did not verify.
*/
c[i] = fBb[i];
assert(c[i] == fBb[i]);
}
/*
error VC8511: Assertion 'a[i] is typed' did not verify.
error VC8512: Assertion 'a[i] is thread local' did not verify.
*/
u = a[i];
assert(u == a[i]);
spec(unsigned long long _spec = clen);
clen = 64;
assert(clen == _spec64);
// How do I verify incremented pointer?
c += 64;
}
if (clen)
{
functionA(fBb, fBa, a);
/*
error VC9502: Call 'functionA(fBb+32, fBa+32, a+32)' did not verify.
error VC9599: (related information) Precondition: '_vcc_is_thread_local_array(b, 32)'.
*/
functionA(fBb+32, fBa+32, a+32);
for (j = 0;j < clen;++j)
invariant((0 <= j) && (j <= clen))
{
/*
error VC8506: Assertion 'c[i] is typed' did not verify.
error VC8507: Assertion 'c[i] is writable' did not verify.
*/
c[j] = fBb[j];
assert(c[j] == fBb[j]);
}
return 0;
}
else
return u;
}
I would be grateful for any help..
<! @page { margin: 0.79in } P { marginbottom: 0.08in } >
I would be grateful for any help..
