On Wed, 2021-06-09 at 22:52 -0700, Andreas Tiemeyer wrote:
> What we are looking for is a version of sizeof() that counts bits
> than bytes. A possible solution would be to implement it as a built-
> CPROVER function like CPROVER_array_copy. I was hoping that such a
> already existed. I guess it was not needed before, because datatypes
> usually have a size that is a multiple of CHAR_BITS.
Yes; the __CPROVER_bitvector types are not particularly widely used so
it might be that you are just the first person to ask. A built-in
function that works like sizeof() is probably the best way to do if you
want the solver to know, rather than just using a macro to define the
size of the bitvector.