Linker does not identify the correct function with external linkage

[andreast271]

CBMC version: 5.82.0
Operating system: Linux x86_64
Exact command line resulting in the issue: cbmc f1.c f2.c f3.c
What behaviour did you expect: VERIFICATION FAILED and no warning about "no body for function ..."
What happened instead: VERIFICATION SUCCESSFUL and a warning about "no body for function f$link2"

In the example code:

• f3.c defines main(), which calls f() which has been declared with external linkage
• f2.c defines f() with external linkage
• f1.c defines a function f() with static linkage

Calling cbmc with --show-goto-functions shows the goto code for main() as:

main /* main */
        // 1 file f3.c line 4 function main
        CALL f$link2()
        // 2 file f3.c line 5 function main
        SET RETURN VALUE 0
        // 3 file f3.c line 6 function main
        END_FUNCTION

However, there is no function f$link2 among the goto functions that are listed.
There are only f (which is the function with internal linkage) and f$link1 (which is the function with external linkage).

f1.c.txt
f2.c.txt
f3.c.txt

[tautschnig]

Looking into this, this resembles a situation I believe I have seen before (but failed to investigate).

[tautschnig]

The bug is that we are failing to retain the linker's state across multiple translation units. I am working on a fix, but until that's deployed the workaround is to have file-local definitions come last in the linking sequence (in your example: f1.c).