File tree Expand file tree Collapse file tree 1 file changed +5
-6
lines changed Expand file tree Collapse file tree 1 file changed +5
-6
lines changed Original file line number Diff line number Diff 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
You can’t perform that action at this time.
0 commit comments