Merge pull request #739 from NlightNFotis/bugfix/static_function

Bugfix/static function

Author: Daniel Kroening

regression/ansi-c/static1/main.c

@@ -0,0 +1,4 @@
+static int fun(int a)
+{
+    return a+1;
+}

regression/ansi-c/static_inline2/test.desc renamed to regression/ansi-c/static1/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 --function fun
 ^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/ansi-c/static2/main.c

@@ -0,0 +1,4 @@
+int foo(int a)
+{
+  return a+1;
+}

regression/ansi-c/static2/main2.c

@@ -0,0 +1,4 @@
+static int foo(int a)
+{
+  return a+1;
+}

regression/ansi-c/static2/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+main2.c --function foo
+^main symbol `foo' is ambiguous$
+--
+^warning: ignoring

regression/ansi-c/static3/main.c

@@ -0,0 +1,4 @@
+static int foo(int a)
+{
+  return a+1;
+}

regression/ansi-c/static3/main2.c

@@ -0,0 +1,4 @@
+static int foo(int a)
+{
+  return a+1;
+}

regression/ansi-c/static3/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.c
+main2.c --function foo
+^main symbol `foo' is ambiguous$
+--
+^warning: ignoring

regression/ansi-c/static_inline1/test.desc

@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/ansi-c/static_inline2/main.c

@@ -0,0 +1,4 @@
+static int foo(int a)
+{
+  return a+1;
+}

regression/cbmc/Static4/main.c

@@ -0,0 +1,7 @@
+CORE
+main.c
+--show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+^Symbol......: foo

regression/cbmc/Static4/test.desc

@@ -213,7 +213,12 @@ void goto_partial_inline(
       // called function
       const goto_functiont &goto_function=f_it->second;
 
-      if(!goto_function.body_available())
+      // 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())
         continue;
 
       const goto_programt &goto_program=goto_function.body;

src/goto-programs/goto_inline.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening
 #include <util/find_symbols.h>
 #include <util/std_types.h>
 #include <util/cprover_prefix.h>
+#include <util/config.h>
 
 #include "remove_internal_symbols.h"
 
@@ -149,7 +150,8 @@ void remove_internal_symbols(
     else if(is_function)
     {
       // body? not local (i.e., "static")?
-      if(has_body && !is_file_local)
+      if(has_body &&
+         (!is_file_local || (config.main==symbol.name.c_str())))
         get_symbols_rec(ns, symbol, exported);
     }
     else