Skip to content

Commit 8110557

Browse files
committed
goto-instrument: Remove inline asm before doing various operations
If mutations such as expanding function pointers have been performed, then removing inline asm is reasonable as well.
1 parent 714ccff commit 8110557

File tree

1 file changed

+4
-6
lines changed

1 file changed

+4
-6
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -838,6 +838,10 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
838838
cmdline.isset("pointer-check"));
839839
status() << "Virtual function removal" << eom;
840840
remove_virtual_functions(goto_model);
841+
status() << "Cleaning inline assembler statements" << eom;
842+
remove_asm(goto_model);
843+
844+
goto_model.goto_functions.update();
841845
}
842846

843847
/// Remove function pointers that can be resolved by analysing const variables
@@ -1213,12 +1217,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
12131217

12141218
if(cmdline.isset("mm"))
12151219
{
1216-
// TODO: move to wmm/weak_mem, and copy goto_functions AFTER some of the
1217-
// modifications. Do the analysis on the copy, after remove_asm, and
1218-
// instrument the original (without remove_asm)
1219-
remove_asm(goto_model);
1220-
goto_model.goto_functions.update();
1221-
12221220
std::string mm=cmdline.get_value("mm");
12231221
memory_modelt model;
12241222

0 commit comments

Comments
 (0)