Fix early return soundness in Laurel: replace assume false with exit

[fabiomadge]

Problem

Early returns in Laurel were encoded as result := value; assume false. The assume false made the return path vacuously true, so Core's VCG never checked postconditions on early return paths. A procedure like:

procedure buggy(x: int) returns (r: int)
  ensures r >= 0
{
  if (x < 0) { return x; }  // violates postcondition — was not caught
  return x;
}

passed verification silently.

Fix

Replace assume false with exit $body targeting a labeled body block. The exit skips remaining body statements, but postconditions — appended after the block by ProcedureEval — are still checked on all paths.

Changes

• LaurelToCoreTranslator: assume "return" false → .exit (some "$body") md, wrap procedure body in labeled $body block
• TestDiagnostics: support consecutive annotation comments targeting the same code line (needed for duplicate diagnostics from Core VCG: goto inside if-then-else causes path multiplication across procedures #419)
• T8b_EarlyReturnPostconditions: test proving the buggy early return is now caught
• T3_ControlFlow: updated annotations for Core VCG: goto inside if-then-else causes path multiplication across procedures #419 duplicate diagnostics

Context

See PR #385 discussion for the original analysis of this soundness issue. Duplicate diagnostics from exit inside if branches are a known Core VCG issue (#419).

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[keyboardDrummer]

Nice, thanks

[keyboardDrummer]

Looks great! Thanks

[atomb]

This seems good to me.