Skip to content

Cleanup of goto_instrument_parse_optionst::instrument_goto_program #6897

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
May 31, 2022
Merged

Cleanup of goto_instrument_parse_optionst::instrument_goto_program #6897

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
677be21
Move namespace declaration close to (single) use
tautschnig May 31, 2022
56944c2
Remove "unwind" option parsing that is no longer required
tautschnig May 31, 2022
7e56e96
Goto-instrument: Remove inline ASM before adding library functions
tautschnig May 31, 2022
5c98272
Goto-instrument: Include the library in function pointer restrictions…
tautschnig May 31, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
62 changes: 30 additions & 32 deletions src/goto-instrument/goto_instrument_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1029,38 +1029,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
// all checks supported by goto_check
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);

// unwind loops
if(cmdline.isset("unwind"))
{
log.status() << "Unwinding loops" << messaget::eom;
options.set_option("unwind", cmdline.get_value("unwind"));
}

{
parse_function_pointer_restriction_options_from_cmdline(cmdline, options);

if(
options.is_set(RESTRICT_FUNCTION_POINTER_OPT) ||
options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
{
label_function_pointer_call_sites(goto_model);

restrict_function_pointers(ui_message_handler, goto_model, options);
}
}

// skip over selected loops
if(cmdline.isset("skip-loops"))
{
log.status() << "Adding gotos to skip loops" << messaget::eom;
if(skip_loops(
goto_model, cmdline.get_value("skip-loops"), ui_message_handler))
throw 0;
}

namespacet ns(goto_model.symbol_table);

// initialize argv with valid pointers
if(cmdline.isset("model-argc-argv"))
{
Expand Down Expand Up @@ -1096,6 +1064,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
std::string(CPROVER_PREFIX) + "CUSTOM_BITVECTOR_ANALYSIS");
}

// remove inline assembler as that may yield further library function calls
// that need to be resolved
remove_asm(goto_model);

// add the library
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
<< messaget::eom;
Expand All @@ -1104,6 +1076,31 @@ void goto_instrument_parse_optionst::instrument_goto_program()
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
}

{
parse_function_pointer_restriction_options_from_cmdline(cmdline, options);

if(
options.is_set(RESTRICT_FUNCTION_POINTER_OPT) ||
options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
{
label_function_pointer_call_sites(goto_model);

restrict_function_pointers(ui_message_handler, goto_model, options);
}
}

// skip over selected loops
if(cmdline.isset("skip-loops"))
{
log.status() << "Adding gotos to skip loops" << messaget::eom;
if(skip_loops(
goto_model, cmdline.get_value("skip-loops"), ui_message_handler))
{
throw 0;
}
}

// now do full inlining, if requested
if(cmdline.isset("inline"))
{
Expand Down Expand Up @@ -1420,6 +1417,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
do_indirect_call_and_rtti_removal();

log.status() << "Pointer Analysis" << messaget::eom;
const namespacet ns(goto_model.symbol_table);
value_set_analysist value_set_analysis(ns);
value_set_analysis(goto_model.goto_functions);

Expand Down