Skip to content

Commit

Permalink
goto-instrument: Remove inline asm before doing various operations
Browse files Browse the repository at this point in the history
If mutations such as expanding function pointers have been performed, then
removing inline asm is reasonable as well.
  • Loading branch information
tautschnig committed Jun 4, 2018
1 parent 1a4fc92 commit 4d67ed5
Showing 1 changed file with 2 additions and 6 deletions.
8 changes: 2 additions & 6 deletions src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -809,6 +809,8 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
cmdline.isset("pointer-check"));
status() << "Virtual function removal" << eom;
remove_virtual_functions(goto_model);
status() << "Cleaning inline assembler statements" << eom;
remove_asm(goto_model);
}

/// Remove function pointers that can be resolved by analysing const variables
Expand Down Expand Up @@ -1184,12 +1186,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()

if(cmdline.isset("mm"))
{
// TODO: move to wmm/weak_mem, and copy goto_functions AFTER some of the
// modifications. Do the analysis on the copy, after remove_asm, and
// instrument the original (without remove_asm)
remove_asm(goto_model);
goto_model.goto_functions.update();

std::string mm=cmdline.get_value("mm");
memory_modelt model;

Expand Down

0 comments on commit 4d67ed5

Please sign in to comment.