Skip to content

Commit ee5fb93

Browse files
author
thk123
committed
Protect against invalid function label
Check the symbol actually exists before trying to regenerate the _start function.
1 parent 2a3d876 commit ee5fb93

File tree

1 file changed

+18
-8
lines changed

1 file changed

+18
-8
lines changed

src/cbmc/cbmc_parse_options.cpp

+18-8
Original file line numberDiff line numberDiff line change
@@ -630,14 +630,24 @@ int cbmc_parse_optionst::get_goto_program(
630630

631631
if(cmdline.isset("function"))
632632
{
633-
const symbolt &desired_entry_function=
634-
symbol_table.lookup(cmdline.get_value("function"));
635-
languaget *language=get_language_from_mode(desired_entry_function.mode);
636-
637-
language->regenerate_start_function(
638-
desired_entry_function,
639-
symbol_table,
640-
goto_functions);
633+
const std::string &function_id=cmdline.get_value("function");
634+
const auto &desired_entry_function=
635+
symbol_table.symbols.find(function_id);
636+
637+
if(desired_entry_function!=symbol_table.symbols.end())
638+
{
639+
languaget *language=get_language_from_mode(
640+
desired_entry_function->second.mode);
641+
language->regenerate_start_function(
642+
desired_entry_function->second,
643+
symbol_table,
644+
goto_functions);
645+
}
646+
else
647+
{
648+
error() << "main symbol `" << function_id;
649+
error() << "' not found" << messaget::eom;
650+
}
641651
}
642652

643653
if(cmdline.isset("show-symbol-table"))

0 commit comments

Comments
 (0)