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

Diff for: src/cbmc/cbmc_parse_options.cpp

@@ -853,6 +853,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))

Diff for: 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))

Diff for: 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))

Diff for: 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);
+    }
   }
 
   {

Diff for: 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);

Diff for: 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(