Difference between local and global arrays access?

Mar 19, 2010 at 5:23 PM

Hi everyone, I have a funny case here that my amateur knowledge of VCC cannot explain so far.

The following program is proven correct:

 

#include <vcc.h>

unsigned char X,A;
unsigned char thearray[6];

void fun(void)
writes(&X)
requires(mutable(as_array(thearray,6)))
requires(mutable(&A))
requires((A>=0 && A<=5)) { X=thearray[A]; assert(false); }

 

Is there a reason for that which I am overseeing? Or is an extra annotation required when accessing global arrays?

the following program complains about the assert(false) as expected:

void fun(void)
writes(&X)
requires(mutable(as_array(thearray,6)))
requires(mutable(&A))
requires((A>=0 && A<=5))
{
    unsigned char arr[6];
    X=arr[A];
    assert(false);
}

Thanks a lot.

Mar 24, 2010 at 9:31 AM

Additionally, it also fails if you assign to a local variable, like in

unsigned char c;
c=thearray[A];
assert(false);

If you remove the assert(false) and use vcc /smoke, it gives:

 Verification of fun succeeded.
 error_arrayassign.c(15): found unreachable code, possible soundness violation, please check the axioms or add an explicit assert(false)
 Found unreachable code, but cannot figure out where it is.

The smoke test yields the same message for the original problem. The used version is:

 Microsoft Research Vcc Version 2.1.30219.0
 Microsoft Research Boogie Version 2.0.20209
 Microsoft Research Z3 Version 2.0.31211.2

Can someone explain if this is an error in the specification or in vcc itself?

Editor
Mar 24, 2010 at 10:09 AM

Hi,
From what I've been able to gather using VCC so far, it seems to have consistency issues with handling global arrays and structures.
Your best bet, if you can do so, is to remove the globals and pass them around as arguments instead. Of course, this does not work if you are not allowed to modify the code...

Cheers,
Francois

Coordinator
Mar 25, 2010 at 9:20 PM
Edited Mar 25, 2010 at 9:23 PM

The global array is no an as_array() object. You can either say "requires(is_mutable_array(thearray, 6))" or try to play with mutable(emb(thearray)). A good test would be to have a main() function, with "requires(program_entry_point())" and try to call your function from there.

BTW, I do agree that our current story for globals and arrays is a mess. We need to do something about it.

Hope this helps!
Michal

Coordinator
Mar 25, 2010 at 9:32 PM

(Some info on globals is on http://vcc.codeplex.com/wikipage?title=Globals&referringTitle=Documentation.)

(On a related note, we might want to get the vcc(as_array) variable attribute working as it does for arrays with primitive element type inside structs, i.e., don't embed the array but turn it into an as_array() object; currently it doesn't work like that but is silently ignored).

Mar 27, 2010 at 9:44 AM

Thank you, this helps a lot!