Merge pull request #862 from NathanJPhillips/bugfix/inlining-errors

Fixed inefficiency and failure to pass on parameter

Author: kroening

src/goto-programs/goto_inline.cpp

@@ -123,10 +123,20 @@ void goto_inline(
 Function: goto_partial_inline
 
   Inputs:
+    goto_model:
+      Source of the symbol table and function map to use.
+    message_handler:
+      Message handler used by goto_inlinet.
+    smallfunc_limit:
+      The maximum number of instructions in functions to be inlined.
+    adjust_function:
+      Tell goto_inlinet to adjust function.
 
  Outputs:
 
  Purpose:
+    Inline all function calls to functions either marked as "inlined" or
+    smaller than smallfunc_limit (by instruction count).
 
 \*******************************************************************/
 
@@ -150,10 +160,23 @@ void goto_partial_inline(
 Function: goto_partial_inline
 
   Inputs:
+    goto_functions:
+      The function map to use to find functions containing calls and function
+      bodies.
+    ns:
+      Namespace used by goto_inlinet.
+    message_handler:
+      Message handler used by goto_inlinet.
+    smallfunc_limit:
+      The maximum number of instructions in functions to be inlined.
+    adjust_function:
+      Tell goto_inlinet to adjust function.
 
  Outputs:
 
  Purpose:
+    Inline all function calls to functions either marked as "inlined" or
+    smaller than smallfunc_limit (by instruction count).
 
 \*******************************************************************/
 
@@ -182,6 +205,10 @@ void goto_partial_inline(
     if(!goto_function.body_available())
       continue;
 
+    if(f_it->first==goto_functions.entry_point())
+      // Don't inline any function calls made from the _start function.
+      continue;
+
     goto_programt &goto_program=goto_function.body;
 
     goto_inlinet::call_listt &call_list=inline_map[f_it->first];
@@ -195,10 +222,10 @@ void goto_partial_inline(
       exprt function_expr;
       exprt::operandst arguments;
       exprt constrain;
-
       goto_inlinet::get_call(i_it, lhs, function_expr, arguments, constrain);
 
       if(function_expr.id()!=ID_symbol)
+        // Can't handle pointers to functions
         continue;
 
       const symbol_exprt &symbol_expr=to_symbol_expr(function_expr);
@@ -208,17 +235,14 @@ void goto_partial_inline(
         goto_functions.function_map.find(id);
 
       if(f_it==goto_functions.function_map.end())
+        // Function not loaded, can't check size
         continue;
 
       // called function
       const goto_functiont &goto_function=f_it->second;
 
-      // We can't take functions without bodies to find functions
-      // inside them to be inlined.
-      // We also don't allow for the _start function to have any of its
-      // function calls to be inlined
-      if(!goto_function.body_available() ||
-         f_it->first==goto_functions.entry_point())
+      if(!goto_function.body_available())
+        // The bodies of functions that don't have bodies can't be inlined.
         continue;
 
       const goto_programt &goto_program=goto_function.body;
@@ -240,36 +264,52 @@ void goto_partial_inline(
 Function: goto_function_inline
 
   Inputs:
+    goto_model: Source of the symbol table and function map to use.
+    function: The function whose calls to inline.
+    message_handler: Message handler used by goto_inlinet.
+    adjust_function: Tell goto_inlinet to adjust function.
+    caching: Tell goto_inlinet to cache.
 
  Outputs:
 
  Purpose:
+    Inline all function calls made from a particular function
 
 \*******************************************************************/
 
 void goto_function_inline(
   goto_modelt &goto_model,
   const irep_idt function,
   message_handlert &message_handler,
-  bool adjust_function)
+  bool adjust_function,
+  bool caching)
 {
   const namespacet ns(goto_model.symbol_table);
   goto_function_inline(
     goto_model.goto_functions,
     function,
     ns,
-    message_handler);
+    message_handler,
+    adjust_function,
+    caching);
 }
 
 /*******************************************************************\
 
 Function: goto_function_inline
 
   Inputs:
+    goto_functions: The function map to use to find function bodies.
+    function: The function whose calls to inline.
+    ns: Namespace used by goto_inlinet.
+    message_handler: Message handler used by goto_inlinet.
+    adjust_function: Tell goto_inlinet to adjust function.
+    caching: Tell goto_inlinet to cache.
 
  Outputs:
 
  Purpose:
+    Inline all function calls made from a particular function
 
 \*******************************************************************/