Difference b/w requires(wrapped(as_array(buf,len) and requires(is_thread_local_array(buf,len))

Mar 14, 2011 at 7:33 PM

In the example of binaryseach.c in Demo folder. What would be the difference in the following two codes. Both of them verify.

 

unsigned binary_search(int val, int *buf, unsigned len)

requires(is_thread_local_array(buf,len))

{-----}

 

or this,

 

unsigned binary_search(int val, int *buf, unsigned len)

requires(wrapped(as_array(buf,len)))

{----}

Editor
Mar 14, 2011 at 8:06 PM

wrapped() is much stronger than thread_local(). In particular, thread locality is lost as soon as any function that can write anywhere in memory is called, whereas the only functions that can unwrap() an object are functions that write that object itself.

I hope this helps.

Francois

Mar 14, 2011 at 8:42 PM

Thanks Francois. Little bit confused. You wanna say that if there is some function which is called inside or outside binary_search which modifies memory, then we could not have used the argument for thread locality in the required clause for the 'buf' array? Or thread locality is lost only if 'buf' is modified?