Remove inline assembler introduced by library functions

Library functions may introduce inline assembler. For example, FreeBSD's
fesetround is an inline function with inline assembler. Library
functions might introduce calls to fesetround, and thereby introduce
inline assembler. Thus, run a fixed point over remove_asm and library
linking.

Author: tautschnig

src/cbmc/cbmc_parse_options.cpp

@@ -878,6 +878,15 @@ bool cbmc_parse_optionst::process_goto_program(
     goto_model, log.get_message_handler(), cprover_cpp_library_factory);
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);
+  // library functions may introduce inline assembler
+  while(has_asm(goto_model))
+  {
+    remove_asm(goto_model);
+    link_to_library(
+      goto_model, log.get_message_handler(), cprover_cpp_library_factory);
+    link_to_library(
+      goto_model, log.get_message_handler(), cprover_c_library_factory);
+  }
 
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -692,6 +692,14 @@ bool goto_analyzer_parse_optionst::process_goto_program(
                << messaget::eom;
   link_to_library(goto_model, ui_message_handler, cprover_cpp_library_factory);
   link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
+  // library functions may introduce inline assembler
+  while(has_asm(goto_model))
+  {
+    remove_asm(goto_model);
+    link_to_library(
+      goto_model, ui_message_handler, cprover_cpp_library_factory);
+    link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
+  }
 
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))

src/goto-diff/goto_diff_parse_options.cpp

@@ -183,6 +183,14 @@ bool goto_diff_parse_optionst::process_goto_program(
                << messaget::eom;
   link_to_library(goto_model, ui_message_handler, cprover_cpp_library_factory);
   link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
+  // library functions may introduce inline assembler
+  while(has_asm(goto_model))
+  {
+    remove_asm(goto_model);
+    link_to_library(
+      goto_model, ui_message_handler, cprover_cpp_library_factory);
+    link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
+  }
 
   // Common removal of types and complex constructs
   if(::process_goto_program(goto_model, options, log))

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1073,6 +1073,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     link_to_library(
       goto_model, ui_message_handler, cprover_cpp_library_factory);
     link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
+    // library functions may introduce inline assembler
+    while(has_asm(goto_model))
+    {
+      remove_asm(goto_model);
+      link_to_library(
+        goto_model, ui_message_handler, cprover_cpp_library_factory);
+      link_to_library(
+        goto_model, ui_message_handler, cprover_c_library_factory);
+    }
   }
 
   {

src/goto-synthesizer/cegis_verifier.cpp

@@ -89,6 +89,15 @@ void cegis_verifiert::preprocess_goto_model()
     goto_model, log.get_message_handler(), cprover_cpp_library_factory);
   link_to_library(
     goto_model, log.get_message_handler(), cprover_c_library_factory);
+  // library functions may introduce inline assembler
+  while(has_asm(goto_model))
+  {
+    remove_asm(goto_model);
+    link_to_library(
+      goto_model, log.get_message_handler(), cprover_cpp_library_factory);
+    link_to_library(
+      goto_model, log.get_message_handler(), cprover_c_library_factory);
+  }
   process_goto_program(goto_model, options, log);
 
   add_failed_symbols(goto_model.symbol_table);

src/libcprover-cpp/api.cpp

@@ -188,6 +188,15 @@ bool api_sessiont::preprocess_model() const
     *implementation->model,
     *implementation->message_handler,
     cprover_c_library_factory);
+  // library functions may introduce inline assembler
+  while(has_asm(*implementation->model))
+  {
+    remove_asm(*implementation->model);
+    link_to_library(
+      *implementation->model,
+      *implementation->message_handler,
+      cprover_c_library_factory);
+  }
 
   // Common removal of types and complex constructs
   if(::process_goto_program(