Array annotations

ptr as_array(ptr p, sz s)

Reinterprete pointer p as in array of the specific size s. This annotation is primarily used for expression of ownership relations. In the Boogie prelude this annotation introduces as new pointer of an array type, which can be used by array annotations.

ptrset array_range(ptr p, sz s)

This function returns a set of pointers of the elements of the array pointed to by p, with s elements. Therefore the returned set contains pointers to all elements of p.

bool is_array(ptr p, sz s)

The functions returns boolean value, whether or not the pointer p can be accessed as an array - with size s elements.

bool is_thread_local_array(ptr p, sz s)

If the pointer p points to an array of size s and all elements of the array are thread_local, this functions returns true. Otherwise false will be returned.

bool is_mutable_array(ptr p, sz s)

If the pointer p points to an array of size s and all elements of the array are mutable, this functions returns true. Otherwise false will be returned.

bool is_array_emb(ptr p, sz s)

To be defined