Regression tests for same-named functions across translation units

[tautschnig]

Static (internal-linkage) functions may share a name across translation units, and may coexist with a global (external-linkage) function of the same name. Extend the existing Static_Functions1 directory with two further test descriptors confirming CBMC's behaviour here:

• test-resolve.desc checks that calls resolve to the definition mandated by the C standard when two translation units each define a file-local f and a third defines a global f: each file-local call stays within its unit, and the call from the unit defining the global reaches it.

• test-unwind.desc checks loop unwinding in this context. Linking renames the second same-named static function, so the two loops carry distinct identifiers count.0 and count$link1.0. The test uses --unwindset with those identifiers to bound the loops independently, demonstrating that the linker-renamed identifier selects the intended loop.

The pre-existing test.desc already covers a static function shadowing a global of the same name.

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

Adds regression coverage for C linkage edge-cases where multiple translation units define same-named static functions, including verifying correct call resolution and demonstrating --unwindset targeting of linker-renamed loop identifiers.

Changes:

• Add a new multi-translation-unit regression test (test-resolve.desc) covering resolution between per-TU static f and a global f.
• Add a new multi-translation-unit unwinding regression test (test-unwind.desc) demonstrating independent loop bounding via count.0 vs count$link1.0.
• Introduce supporting C sources for both scenarios under regression/cbmc/Static_Functions1/.

Reviewed changes

Copilot reviewed 8 out of 8 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
regression/cbmc/Static_Functions1/resolve_main.c	Defines global f and asserts correct resolution across TUs.
regression/cbmc/Static_Functions1/resolve_a.c	Provides a TU-local static f and wrapper fa().
regression/cbmc/Static_Functions1/resolve_b.c	Provides a TU-local static f and wrapper fb().
regression/cbmc/Static_Functions1/test-resolve.desc	Checks CBMC resolves each call to the correct linkage target.
regression/cbmc/Static_Functions1/unwind_main.c	Drives both entrypoints and asserts expected results.
regression/cbmc/Static_Functions1/unwind_a.c	Provides first TU-local static count loop (expected loop id count.0).
regression/cbmc/Static_Functions1/unwind_b.c	Provides second TU-local static count loop (expected loop id count$link1.0).
regression/cbmc/Static_Functions1/test-unwind.desc	Validates --unwindset can independently bound the two loops.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.78%. Comparing base (34bf21c) to head (872a2e2).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9106   +/-   ##
========================================
  Coverage    80.77%   80.78%           
========================================
  Files         1712     1712           
  Lines       189814   189814           
  Branches        73       73           
========================================
+ Hits        153328   153332    +4     
+ Misses       36486    36482    -4     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.