CBMC should have a `r_ok` primitive that is indexed by number of elements, not number of bytes

[danielsn]

Often, we want to check that we can read the nth element of an array. Currently, we need __CPROVER_r_ok(ptr, index * sizeof(*ptr)), which can lead to overflow issues and weird error messages to users. Instead, we would like

__CPROVER_r_ok_array(ptr, num_elements)

Feel free to bikeshed the name!

[tautschnig]

I'm aware that we've spoken about this more than once, but it only now occurred to me that with such a new intrinsic we'd also have separately specify the overflow behaviour. That, in turn, makes me wonder whether adding support for this really is the right thing to do.

[kroening]

Overflow is already a problem with the byte variant. I'd say that the predicate should evaluate to false when there's overflow.