From f507eaef68b72a745cb1ecd9f9c157e05d41ae4f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 14 Feb 2022 11:16:34 +0000 Subject: [PATCH] C nondet symbol factory: arrays may have zero size There is nothing fundamentally wrong in an array having size 0. Also, do not assume that size has an unsigned type. Fixes: #5093 --- .../test.desc | 7 +++---- src/ansi-c/c_nondet_symbol_factory.cpp | 8 +++++--- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc b/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc index cf33b414d58..e792512536c 100644 --- a/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc +++ b/regression/cbmc/pointer-to-struct-with-flexible-array-member-as-parameter-to-entry-point/test.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE main.c --function testFunc --- ^EXIT=0$ ^SIGNAL=0$ -- -^EXIT=134$ -- -Github issue #5093: Pointer to struct with flexible array member as parameter to entry point causes invariant violation +Github issue #5093: Pointer to struct with flexible array member as parameter to +entry point causes invariant violation diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp index 931ce331718..a7d7fcd4078 100644 --- a/src/ansi-c/c_nondet_symbol_factory.cpp +++ b/src/ansi-c/c_nondet_symbol_factory.cpp @@ -172,9 +172,11 @@ void symbol_factoryt::gen_nondet_array_init( auto const &array_type = to_array_type(expr.type()); const auto &size = array_type.size(); PRECONDITION(size.id() == ID_constant); - auto const array_size = numeric_cast_v(to_constant_expr(size)); - DATA_INVARIANT(array_size > 0, "Arrays should have positive size"); - for(size_t index = 0; index < array_size; ++index) + auto const array_size = numeric_cast(to_constant_expr(size)); + DATA_INVARIANT( + array_size.has_value() && *array_size >= 0, + "Arrays should have positive size"); + for(mp_integer index = 0; index < *array_size; ++index) { gen_nondet_init( assignments,