Inliner fixes

smowton · Feb 23, 2018 · bc2c0cd · bc2c0cd
1 parent 0003d8a
commit bc2c0cd
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 23 deletions.
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -992,7 +992,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   // now do full inlining, if requested
   if(cmdline.isset("inline"))
   {
-    do_indirect_call_and_rtti_removal();
+    do_indirect_call_and_rtti_removal(/*force=*/true);
 
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))
@@ -1003,7 +1003,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     }
 
     status() << "Performing full inlining" << eom;
-    goto_inline(goto_model, get_message_handler());
+    goto_inline(goto_model, get_message_handler(), true);
   }
 
   if(cmdline.isset("show-custom-bitvector-analysis") ||
@@ -1111,27 +1111,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   if(cmdline.isset("partial-inline"))
   {
     do_indirect_call_and_rtti_removal();
-    do_partial_inlining();
 
-    goto_model.goto_functions.update();
-    goto_model.goto_functions.compute_loop_numbers();
-  }
-
-  // now do full inlining, if requested
-  if(cmdline.isset("inline"))
-  {
-    do_indirect_call_and_rtti_removal(/*force=*/true);
+    status() << "Partial inlining" << eom;
+    goto_partial_inline(goto_functions, ns, ui_message_handler, 0, true);
 
-    if(cmdline.isset("show-custom-bitvector-analysis") ||
-       cmdline.isset("custom-bitvector-analysis"))
-    {
-      do_remove_returns();
-      thread_exit_instrumentation(goto_model);
-      mutex_init_instrumentation(goto_model);
-    }
-
-    status() << "Performing full inlining" << eom;
-    goto_inline(goto_model, get_message_handler(), true);
+    goto_functions.update();
+    goto_functions.compute_loop_numbers();
   }
 
   if(cmdline.isset("constant-propagator"))

diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp
@@ -79,7 +79,7 @@ void goto_inline(
 
     Forall_goto_program_instructions(i_it, goto_program)
     {
-      if(!i_it->is_function_call())
+      if(!goto_inlinet::is_call(i_it))
         continue;
 
       call_list.push_back(goto_inlinet::callt(i_it, false));

diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h
@@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H