Skip to content

Commit b7f3f2d

Browse files
tautschnigDaniel Kroening
authored and
Daniel Kroening
committed
Support non-constant array sizes in zero initializer
We can use ARRAY_OF for those, just like we do for infinitely large arrays. Fixes: #4603
1 parent 1da804b commit b7f3f2d

File tree

2 files changed

+8
-10
lines changed

2 files changed

+8
-10
lines changed

regression/cbmc-library/calloc-02/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,10 @@ int main()
66
char *p = calloc(-1, -1);
77
if(p)
88
assert(p[0] == 0);
9+
10+
size_t size;
11+
size_t num;
12+
p = calloc(size, num);
13+
if(p && size > 0 && num > 0)
14+
assert(p[0] == 0);
915
}

src/util/expr_initializer.cpp

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,8 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
132132
if(!tmpval.has_value())
133133
return {};
134134

135-
if(array_type.size().id()==ID_infinity)
135+
const auto array_size = numeric_cast<mp_integer>(array_type.size());
136+
if(array_type.size().id() == ID_infinity || !array_size.has_value())
136137
{
137138
if(nondet)
138139
return side_effect_expr_nondett(type, source_location);
@@ -142,15 +143,6 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
142143
return std::move(value);
143144
}
144145

145-
const auto array_size = numeric_cast<mp_integer>(array_type.size());
146-
if(!array_size.has_value())
147-
{
148-
if(nondet)
149-
return side_effect_expr_nondett(type, source_location);
150-
else
151-
return {};
152-
}
153-
154146
if(*array_size < 0)
155147
return {};
156148

0 commit comments

Comments
 (0)