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.

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -845,6 +845,11 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
   remove_exceptions(goto_model);
   status() << "Java instanceof removal" << eom;
   remove_instanceof(goto_model);
+  status() << "Cleaning inline assembler statements" << eom;
+  remove_asm(goto_model);
+
+  goto_model.goto_functions.update();
+  goto_model.goto_functions.compute_loop_numbers();
 }
 
 /// Remove function pointers that can be resolved by analysing const variables
@@ -1220,12 +1225,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;
 

src/goto-programs/remove_asm.cpp

@@ -22,6 +22,8 @@ Date:   December 2014
 
 #include <assembler/assembler_parser.h>
 
+#include "remove_skip.h"
+
 class remove_asmt
 {
 public:
@@ -281,20 +283,29 @@ void remove_asmt::process_instruction(
 void remove_asmt::process_function(
   goto_functionst::goto_functiont &goto_function)
 {
+  bool did_something = false;
+
   Forall_goto_program_instructions(it, goto_function.body)
   {
     if(it->is_other() && it->code.get_statement()==ID_asm)
     {
       goto_programt tmp_dest;
       process_instruction(*it, tmp_dest);
       it->make_skip();
+      did_something = true;
 
       goto_programt::targett next=it;
       next++;
 
       goto_function.body.destructive_insert(next, tmp_dest);
     }
   }
+
+  if(did_something)
+  {
+    remove_skip(goto_function.body);
+    goto_function.body.update();
+  }
 }
 
 /// removes assembler