goto-analyzer: fix reachable-functions analysis for inline functions

regression/goto-analyzer/reachable-functions-stdio-empty/test.c

@@ -0,0 +1,6 @@
+#include <stdio.h>
+
+int main()
+{
+  return 0;
+}

regression/goto-analyzer/reachable-functions-stdio-empty/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.c
+--reachable-functions
+test\.c main [0-9]+ [0-9]+$
+<built-in-additions> __CPROVER_initialize [0-9]+ [0-9]+$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+__sputc

src/goto-analyzer/unreachable_instructions.cpp

@@ -181,9 +181,12 @@ void unreachable_instructions(
 
     const symbolt &decl = ns.lookup(gf_entry.first);
 
-    if(
-      called.find(decl.name) != called.end() ||
-      to_code_type(decl.type).get_inlined())
+    // Only consider functions reachable if they're actually called.
+    // Previously, functions marked as "inline" were automatically treated as
+    // reachable, but this caused false positives on systems (like MacOS) where
+    // system headers contain uncalled inline functions that reference other
+    // functions, making those referenced functions appear reachable.
+    if(called.find(decl.name) != called.end())
     {
       unreachable_instructions(goto_program, dead_map);
     }
@@ -314,9 +317,9 @@ static void list_functions(
   {
     const symbolt &decl = ns.lookup(gf_entry.first);
 
-    if(
-      unreachable == (called.find(decl.name) != called.end() ||
-                      to_code_type(decl.type).get_inlined()))
+    // Only consider functions reachable if they're actually called.
+    // See comment in unreachable_instructions() for rationale.
+    if(unreachable == (called.find(decl.name) != called.end()))
     {
       continue;
     }