From 491d3075ab10bc18f43f7d427f6f123d4f8358e4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 30 Nov 2025 14:18:47 +0000
Subject: [PATCH] goto-analyzer: fix reachable-functions analysis for inline
 functions

We now only consider functions reachable when they are actually called,
and don't automatically consider `inline` functions reachable.

Fixes: #5173
---
 .../reachable-functions-stdio-empty/test.c        |  6 ++++++
 .../reachable-functions-stdio-empty/test.desc     | 10 ++++++++++
 src/goto-analyzer/unreachable_instructions.cpp    | 15 +++++++++------
 3 files changed, 25 insertions(+), 6 deletions(-)
 create mode 100644 regression/goto-analyzer/reachable-functions-stdio-empty/test.c
 create mode 100644 regression/goto-analyzer/reachable-functions-stdio-empty/test.desc

diff --git a/regression/goto-analyzer/reachable-functions-stdio-empty/test.c b/regression/goto-analyzer/reachable-functions-stdio-empty/test.c
new file mode 100644
index 00000000000..5a132bbeb45
--- /dev/null
+++ b/regression/goto-analyzer/reachable-functions-stdio-empty/test.c
@@ -0,0 +1,6 @@
+#include <stdio.h>
+
+int main()
+{
+  return 0;
+}
diff --git a/regression/goto-analyzer/reachable-functions-stdio-empty/test.desc b/regression/goto-analyzer/reachable-functions-stdio-empty/test.desc
new file mode 100644
index 00000000000..a417d1ccb7e
--- /dev/null
+++ b/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
diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp
index 5f0cc4b8fff..958f56adb65 100644
--- a/src/goto-analyzer/unreachable_instructions.cpp
+++ b/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;
     }