Programmatic expression for the size of a CPROVER_bitvector

11 views
Skip to first unread message

Andreas Tiemeyer

unread,
Jun 7, 2021, 3:00:14 AM6/7/21
to CProver Support
I am using CPROVER_bitvector for implementing operations on integers of arbitrary bounds, as found in e.g. the SystemC integer data types. 
For the implementation it would be useful to express the size of a CPROVER_bitvector programatically, for example with something like
CPROVER_bitvector[243] bv;
int size = CPROVER_size(bv);
where the value of size would be 243.
Is something like this supported, or if not can someone suggest a work-around?

Thank you in advance,
Andreas

Martin Nyx Brain

unread,
Jun 7, 2021, 4:57:59 AM6/7/21
to cprover...@googlegroups.com
sizeof(bv) * CHAR_BITS should work but will give you it rounded up to
bytes. Alternatively:

#define BVSIZE 243
CPROVER_bitvector[BVSIZE] bv;

should work and has the option to set the size at analysis type from
the cbmc command-line:

cbmc -DBVSIZE=243 whatever.c

HTH

Cheers,
- Martin


Andreas Tiemeyer

unread,
Jun 10, 2021, 1:52:46 AM6/10/21
to CProver Support
What we are looking for is a version of sizeof() that counts bits rather than bytes. A possible solution would be to implement it as a built-in CPROVER function like CPROVER_array_copy. I was hoping that such a function already existed. I guess it was not needed before, because datatypes usually have a size that is a multiple of CHAR_BITS.

Andreas

Martin Nyx Brain

unread,
Jun 11, 2021, 5:36:05 AM6/11/21
to cprover...@googlegroups.com
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
> rather
> than bytes. A possible solution would be to implement it as a built-
> in
> CPROVER function like CPROVER_array_copy. I was hoping that such a
> function
> 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.

Cheers,
- Martin


Reply all
Reply to author
Forward
0 new messages