# How to verify complex return value

 MarianKuhnel 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 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 ((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 == _spec-64); // 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.. ``` `I would be grateful for any help..`