goto-instrument --apply-loop-contracts aborts (instrument_spec_assigns.h:286) when the loop write set is inferred (regression 6.3.1 → 6.6.0) #9154

I found this issue while applying CBMC loop contracts to unit proofs of embedded operating systems with AI assistance (Claude Code). This report was drafted by AI; the reproducer and the results below were run on the versions listed.

goto-instrument --apply-loop-contracts aborts with an invariant violation in instrument_spec_assigns.h when instrumenting loops that have __CPROVER_loop_invariant and __CPROVER_decreases clauses but no __CPROVER_assigns clause, so that the loop write set is inferred. The same GOTO binary is instrumented cleanly by 6.3.1, so this is a regression.

Tested with the official Ubuntu 22.04 packages of 6.6.0 (fails) and 6.3.1 (works). It still fails on develop at d1451f2.

Reproducer

The attached cfs_open3.goto was built with goto-cc 6.6.0 (-m32) from the attached source.annotated.c, a file from an open-source embedded OS with five loop contracts added. source.original.c is the unannotated file.

goto-instrument --apply-loop-contracts --loop-contracts-no-unwind \
    --slice-global-inits cfs_open3.goto out.goto

Actual behavior

--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-instrument/contracts/instrument_spec_assigns.h:286 function: update
Condition: source_location.is_not_nil()
Reason: Precondition
--- end invariant violation report ---
Aborted (core dumped)

The full output, including the backtrace, is in the attached goto-instrument-6.6.0-abort.txt.

Expected behavior

Instrumentation completes, as it does with 6.3.1 on the same binary and with the same options.

Notes

• The annotated loops are ordinary counter loops, for example:

  for(i = 0; i < MAX_OPEN_FILES; i++)
    __CPROVER_loop_invariant(0 <= i)
    __CPROVER_loop_invariant(i <= MAX_OPEN_FILES)
    __CPROVER_decreases(MAX_OPEN_FILES - i)
  {
    ...
  }

• The abort needs a combination of contracts.

  • No single annotated loop triggers it.
  • Of the five contracted loops in source.annotated.c, four are each necessary: removing the contract from any one of them avoids the abort.
  • The fifth can be replaced by any of several other loops of the same file, but not by loops that are unreachable from the entry function.
  • It is not a count threshold: nine contracted loops instrument fine if one of the four necessary ones is left out.

• I could not reduce this to a small self-contained program. A synthetic program with the same structure (five contracted loops across mutually calling functions, body-less callees, struct locals written through them) instruments cleanly, so the binary is attached instead.

• Workarounds:

  • Adding an explicit __CPROVER_assigns clause to each of the five loops avoids the abort. This points at the write-set inference rather than at the instrumentation of a user-supplied clause.
  • Using goto-instrument 6.3.1 for this step also works.
  • Removing --loop-contracts-no-unwind or adding --unwind 2 does not help.

• Related: goto-instrument --apply-loop-contracts aborts (local_may_alias.cpp) on a GOTO binary previously processed by --unwindset #9217 is another abort reached through write-set inference in the same instrumentation. Its fix (Fix invariant violations in loop assigns inference of --apply-loop-contracts (#9154, #9217) #9218) does not change the behavior on this binary.

cbmc-repro-instrument-assigns.zip