Unwinding

Key Concepts covers what unwinding is and why a bounded proof needs it. This page is about the knobs, for when the default isn’t enough.

The default does the work

You don’t normally set anything. By default each proof tries increasing bounds until its loops are fully covered, then verifies. A loop it can’t cover within the cap comes back Unknown, never a false Verified. It reports the bound it settled on.

This however comes at the cost of slower proofs, as we have to try and interate each attempt.

When to step in

• Skip the search. Once you know the bound, pin it so the proof stops climbing every run: @BmcProof(unwind = 8).

• Go past the cap. A deep loop that needs more than the default cap, but you still want auto-discovery: raise it with @BmcProof(unwindMax = 64) instead of pinning.

• One loop is the problem. When a method has several loops and only one needs a high bound, pin that single loop and leave the rest on auto:

  @LoopUnwind(loop = "java::com.acme.Parser.scan:()V.0", bound = 32)

  The loop id is java::<class>.<method>:<descriptor>.<n>, where n numbers the loops in the method. @LoopUnwind is repeatable, so you can pin several. These pins will be printed on test execution, so you can run it in auto-wind mode once and extract the loop pins.

Whatever you set, unwindingAssertions stays on by default, so an under-explored loop is reported Unknown rather than passed off as Verified. The full attribute list is in Proof annotations; the project-wide defaults are in the plugin config.