[feliperodri]

What

When applying loop contracts, a loop without a contract is skipped (not abstracted) and shares its enclosing scope's write set. dfcc_cfg_infot::get_tracked_set and get_local_set resolved the active scope from the raw loop id, while get_write_set resolved outward through skipped loops via get_first_id_not_skipped_or_top_level_id. Inside a skipped loop these disagreed about which scope was active, so writes to a skipped loop's locals were checked against the enclosing loop's assigns clause and failed spuriously.

This surfaces for a callee that contains a contract-less loop — for example CBMC's built-in memcmp model, whose loop is unwound at solve time — invoked from within a loop that has a contract. The callee's loop locals (res, sc1, sc2, ...) are reported as not assignable even though they are genuinely local. Originally reported against Kani, where slice == slice lowers to the memcmp model: model-checking/kani#4790.

Fix

• get_tracked_set / get_local_set: resolve the active scope through skipped loops (get_first_id_not_skipped_or_top_level_id), matching get_write_set.
• gen_dfcc_loop_info: keep skipped inner loops' locals instead of excluding them (they are not abstracted, so they belong to the enclosing scope).
• Top-level DECL collection: treat DECLs declared in skipped loops whose enclosing non-skipped scope is the top level as top-level locals.

Testing

New regression test regression/contracts-dfcc/loop_contracts_callee_with_loop: an outer loop with a contract calls a helper containing a contract-less loop. The helper's loop locals must be scoped to the callee. The test fails without the fix (4 spurious cmp.assigns ... : FAILURE, VERIFICATION FAILED) and passes with it, and its "forbidden patterns" block asserts no cmp.assigns ... is assignable: FAILURE remains.

---

• Each commit message has a non-empty body, explaining why the change was made.
• Regression tests are included, in the same commit as the fix.
• My PR is restricted to a single bugfix.
• No unrelated white-space or formatting changes.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.83%. Comparing base (820ff0f) to head (09fe194).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9164   +/-   ##
========================================
  Coverage    80.83%   80.83%           
========================================
  Files         1717     1717           
  Lines       190069   190074    +5     
  Branches        73       73           
========================================
+ Hits        153647   153653    +6     
+ Misses       36422    36421    -1     

☔ 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.