Documentation shows loop contracts on do/while loops, but they are rejected: the documented syntax does not parse, and do/while is unsupported by goto-instrument

[rcalvom]

Documentation presents loop invariants on do/while loops, but they are not supported

Summary

The loop-contracts documentation shows a do/while example alongside the while and for ones, with no note distinguishing it. In practice do/while loops cannot carry a loop invariant at all: the documented syntax is rejected by goto-cc as a parse error, and the only placement that does parse is rejected by goto-instrument with Loop contracts are unsupported on do/while loops.

Either the documentation or the implementation should change, and the documentation is presumably the smaller fix.

What the documentation shows

https://diffblue.github.io/cbmc/contracts-loop-invariants.html gives this as the do/while form:

do { ... }
while (i < n)
__CPROVER_loop_invariant(0 <= i)
__CPROVER_loop_invariant(i <= n);

The page states that "invariant clauses may be specified just after the loop guard", and lists no unsupported loop forms.

What happens

Following the documentation:

/* doc.c */
int f(int n){ int i=0; do { i++; } while(i<n) __CPROVER_loop_invariant(i<=n); return i; }

$ goto-cc -c -o doc.goto doc.c
doc.c: In function 'f':
doc.c:1:1: error: syntax error before '__CPROVER_loop_invariant'

The only placement that the parser accepts puts the clause between do and the body, which the documentation does not mention:

/* alt.c */
int f(int n){ int i=0; do __CPROVER_loop_invariant(i<=n) { i++; } while(i<n); return i; }

$ goto-cc -c -o alt.goto alt.c            # accepted
$ goto-instrument --apply-loop-contracts alt.goto out.goto
Loop contracts are unsupported on do/while loops: file alt.c line 1 function f

Tested with CBMC 6.6.0 on Ubuntu 22.04, x86-64.

Expected

Either the documented syntax parses and do/while loops are instrumented, or the documentation states that do/while loops are not supported and keeps only the while and for examples.

Why the current state is hard to diagnose

The two messages arrive in an unhelpful order. A user who follows the documentation hits the goto-cc parse error first, and that error names only the clause, so it reads as a mistake in the annotation rather than as an unsupported loop form. The clear message, the one from goto-instrument, is only reachable after independently guessing a different placement. Stating the limitation in the documentation would remove that detour entirely.

do/while is the natural shape whenever the body must run once before the continuation condition can be evaluated, so the limitation is worth stating explicitly rather than leaving it to be discovered.