Skip to content

Commit f79f501

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 3e2ab6f commit f79f501

File tree

1 file changed

+5
-6
lines changed

1 file changed

+5
-6
lines changed

src/goto-instrument/goto_instrument_parse_options.cpp

+5-6
Original file line numberDiff line numberDiff line change
@@ -846,6 +846,11 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
846846
remove_exceptions(goto_model);
847847
status() << "Java instanceof removal" << eom;
848848
remove_instanceof(goto_model);
849+
status() << "Cleaning inline assembler statements" << eom;
850+
remove_asm(goto_model);
851+
852+
goto_model.goto_functions.update();
853+
goto_model.goto_functions.compute_loop_numbers();
849854
}
850855

851856
/// Remove function pointers that can be resolved by analysing const variables
@@ -1221,12 +1226,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
12211226

12221227
if(cmdline.isset("mm"))
12231228
{
1224-
// TODO: move to wmm/weak_mem, and copy goto_functions AFTER some of the
1225-
// modifications. Do the analysis on the copy, after remove_asm, and
1226-
// instrument the original (without remove_asm)
1227-
remove_asm(goto_model);
1228-
goto_model.goto_functions.update();
1229-
12301229
std::string mm=cmdline.get_value("mm");
12311230
memory_modelt model;
12321231

0 commit comments

Comments
 (0)