Document loop-invariant expections with `break` (and `goto`)

[tautschnig]

We should document that we follow the non-strict approach (in the language of https://whileydave.com/2014/05/02/loop-invariants-and-break-statements/). This can be observed on the following example (courtesy of @hanno-becker):

#define __loop__(x) x

int harness(int n)
{
    __CPROVER_assume(n <= 20);
    int sum = 0;

    for (int i = 0; i < n; i++)
    __loop__(
        __CPROVER_assigns(i, sum)
        __CPROVER_loop_invariant(i >= 0 && i <= n)
        __CPROVER_loop_invariant(sum >= 0 && sum <= 100)
    )
    {
      if(sum +i <= 100)
        sum += i;

        if (sum > 100) {
            // Breaking here violates the invariant (sum > 100)
            break;
        }
    }
    __CPROVER_assert(sum <= 100, "claimed by loop invariant");

    return sum;
}

CBMC does not report a failing loop invariant, but correctly disproves the assertion after the loop, confirming sound behaviour.

Note that https://diffblue.github.io/cbmc/contracts-loop-invariants.html#autotoc_md107 does include a break statement, but does not explicitly talk about the implications thereof.

Edit: that documentation piece retains the break statement in the transformed code example, where we don't have a loop anymore, and break is hence no longer syntactically valid. It should be rewritten using goto.