\mutable_array() and \thread_local_array()

Dec 14, 2011 at 2:16 PM

Hi all,

I'm having trouble with the two predicates in the title and VCC3. Is it no longer true that \mutable_array(p,l) implies \thread_local_array(p,l)?

For example, the following assertion fails to verify:

#include <vcc.h>

void bar(unsigned char* foo,size_t fool)
_(requires \mutable_array(foo,fool))
{ _(assert \thread_local_array(foo,fool)) }

I dug a bit in the Boogie definitions, and it looks like they currently prevent a sub-array from being thread local, as it requires the pointer to be proper. Please let me know if this is an expected behaviour of VCC and what I should use instead, or if this is a bug and expected to be fixed at some point.



Dec 14, 2011 at 3:06 PM

Hi Francois,

  http://vcc.codeplex.com/workitem/6390 / change 1d1abb9b2ca9 is related. The change allowed \mutable_array() to be true for zero array size, but didn't change the behavior for \thread_local_array(), possibly an oversight.

  Your example works as is for _(requires 0 < fool).

  Cheers, Mark

Dec 14, 2011 at 3:41 PM

Thanks a lot for pointing it out.
I did think about this in my debugging thought process but apparently never acted on it.