From 4d67ed576ebed27366ac6f17ce52dcbfb3a76451 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 19 Apr 2018 09:17:40 +0100 Subject: [PATCH] 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. --- src/goto-instrument/goto_instrument_parse_options.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 38e5c8ee588..2b80bd3969a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -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 @@ -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;