Skip to content

Commit c14b2a2

Browse files
NathanJPhillipsOwen Jones
authored and
Owen Jones
committed
Fix crash when no entry point found for LVSA
1 parent a2ca1a3 commit c14b2a2

File tree

1 file changed

+12
-6
lines changed

1 file changed

+12
-6
lines changed

src/driver/sec_driver_parse_options.cpp

Lines changed: 12 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -109,10 +109,13 @@ void sec_driver_parse_optionst::get_command_line_options(optionst &options)
109109

110110
static irep_idt get_cprover_start_main_callee(const goto_modelt &goto_model)
111111
{
112-
const goto_programt &start_body =
113-
goto_model.get_goto_functions().function_map.at(
114-
goto_functionst::entry_point()).body;
112+
const goto_functionst::function_mapt &function_map =
113+
goto_model.get_goto_functions().function_map;
114+
auto entry_it = function_map.find(goto_functionst::entry_point());
115+
if(entry_it == function_map.end())
116+
return {};
115117

118+
const goto_programt &start_body = entry_it->second.body;
116119
auto last_call_it =
117120
std::find_if(
118121
start_body.instructions.rbegin(),
@@ -242,12 +245,15 @@ int sec_driver_parse_optionst::doit()
242245
local_value_set_analysist::dbt summarydb(serializer, 30);
243246
namespacet ns(goto_model.symbol_table);
244247

245-
const std::string function_name = cmdline.get_value("function");
246248
const bool print_function_summary = cmdline.isset("show-value-sets");
247249
const bool print_all_summaries = cmdline.isset("show-value-sets-all");
248250

249-
irep_idt fully_qualified_name =
250-
get_cprover_start_main_callee(goto_model);
251+
irep_idt fully_qualified_name = get_cprover_start_main_callee(goto_model);
252+
if(fully_qualified_name.empty())
253+
{
254+
error() << "You must specify an entry point with --function" << eom;
255+
return CPROVER_EXIT_USAGE_ERROR;
256+
}
251257

252258
call_grapht const call_graph(goto_model.goto_functions);
253259
std::vector<irep_idt> process_order =

0 commit comments

Comments
 (0)