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 + +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]+$ + __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; }