Jun 21, 2011 at 2:22 PM
Edited Jun 21, 2011 at 2:27 PM

Hi Mark,
It's always hard for me to figure out where extra guidence is needed for VCC to pass the verification. Do you have any suggestions?
For example, for checking if two arrays are equal, VCC verifys eq2, but fails eq1. Sorry for the format, somehow I couldn't paste the code in correct format.
Thanks.
int eq1(int *ar1, unsigned len1, int *ar2, unsigned len2)
_(requires \thread_local_array(ar1,len1))
_(requires \thread_local_array(ar2,len2))
_(returns (len1 == len2) && (\forall unsigned i; i < len1 ==> ar1[i] == ar2[i]))
{
if (len1 != len2) {
return 0;
}
if (len1 <= 0) return 1; //otherwise can't prove ar1[len11] is readable
if (ar1[0] != ar2[0]) {
return 0;
} else {
int t = ex2(ar1+1,len11,ar2+1,len21);
_(assert \forall unsigned i; 0 < i && i < len11 ==> ar1[i] == (ar1+1)[i1])
_(assert \forall unsigned i; 0 < i && i < len21 ==> ar2[i] == (ar2+1)[i1])
return t;
}
}
//check for equal arrays
int eq2(int *ar1, unsigned len1, int *ar2, unsigned len2)
_(requires \thread_local_array(ar1,len1))
_(requires \thread_local_array(ar2,len2))
_(returns (len1 == len2) && (\forall unsigned i; i < len1 ==> ar1[i] == ar2[i]))
{
if (len1 != len2) {
return 0;
}
if (len1 <= 0) return 1; //otherwise can't prove ar1[len11] is readable
if (ar1[len11] != ar2[len21]) {
return 0;
} else {
return ex2(ar1,len11,ar2,len21);
}
}
