Skip to content

Commit 014b099

Browse files
committed
ansi_c_entry_point: avoid magic number
The code previously hard-coded an upper bound for argc that perhaps was suitable for 32-bit systems (albeit even questionable for that case). Replace this calculation by one that refers to configured bit widths.
1 parent 6e88f92 commit 014b099

File tree

1 file changed

+11
-3
lines changed

1 file changed

+11
-3
lines changed

src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -311,10 +311,18 @@ bool generate_ansi_c_start_function(
311311
init_code.add(code_assumet(std::move(ge)));
312312
}
313313

314+
// assume argc is no larger than the what would make argv consume all
315+
// available memory space:
316+
// 2^pointer_width / (pointer_width / char_width)
317+
// is the maximum number of argv elements
318+
const auto pointer_bits_2log =
319+
address_bits(config.ansi_c.pointer_width / config.ansi_c.char_width);
320+
if(
321+
config.ansi_c.pointer_width - pointer_bits_2log <=
322+
config.ansi_c.int_width)
314323
{
315-
// assume argc is at most MAX/8-1
316-
mp_integer upper_bound=
317-
power(2, config.ansi_c.int_width-4);
324+
mp_integer upper_bound =
325+
power(2, config.ansi_c.int_width - pointer_bits_2log);
318326

319327
exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
320328

0 commit comments

Comments
 (0)