gen_nondet_array_init: arrays may have size 0 #5342
Conversation
The various C standards clearly allow arrays of size 0.
This prevents a dependency of the analysis on the architecture that CBMC has been compiled for.
|
Zero-length arrays are not allowed in standard C. It's a common enough extension to allow 0 as the size, but in that case it's normally used to denote arrays of variable length rather than zero length (https://gcc.gnu.org/onlinedocs/gcc-4.7.2/gcc/Zero-Length.html). Since gcc allows it we probably should too though. |
| @@ -173,7 +173,7 @@ void symbol_factoryt::gen_nondet_array_init( | |||
| const auto &size = array_type.size(); | |||
| PRECONDITION(size.id() == ID_constant); | |||
| auto const array_size = numeric_cast_v<size_t>(to_constant_expr(size)); | |||
| DATA_INVARIANT(array_size > 0, "Arrays should have positive size"); | |||
| DATA_INVARIANT(array_size >= 0, "Arrays must have non-negative size"); | |||
There was a problem hiding this comment.
Could we please have a test that covers the case of size 0?
There was a problem hiding this comment.
Just a note to perhaps help make progress on this one: I believe #4928 has such a test.
| DATA_INVARIANT(array_size >= 0, "Arrays must have non-negative size"); | ||
| for(size_t index = 0; index < array_size; ++index) | ||
| for(mp_integer index = 0; index < array_size; ++index) |
There was a problem hiding this comment.
While this makes sense in spirit, does this actually make a difference in practice (other than slightly worse performance)? We wouldn't be able to allocate memory for an object larger than max(size_t) anyway.
The various C standards clearly allow arrays of size 0.