Laurel User Guide

10.2. Accepted today, but limited🔗

These parse and resolve, so nothing warns you early, and they fail or misbehave later:

  • float64 parses and resolves, but is not implemented, so it cannot reach an analysis.

  • Bitvector literals, storage, equality, and comparisons work, and comparisons are signed. General bitvector arithmetic does not yet select the bitvector operator family, and comparisons exist only at widths 1, 8, 16, 32, and 64.

  • For real, the implemented operators are +, -, *, /, unary -, and the orderings. %, /t, and %t are admitted by resolution but are not correctly implemented.

  • A composite field declared without var is not protected from writes.

  • new should be used only with composites, even though the resolver also accepts datatypes.

  • A composite field whose type is a generic datatype instantiation is rejected, because the heap representation cannot distinguish instantiations.

  • A transparent procedure's body is turned into a function only for supported control and effect shapes; opaque is the robust choice for imperative code.

  • Passing too few arguments to a procedure is not currently diagnosed, while passing too many is. Always pass exactly the declared number.

  • Effects in a loop condition, control flow in a block used as a value, and assert/assume in the right-hand side of a short-circuit operator all misbehave; each is described where the construct itself is, under Execution.

  • Do not shadow a procedure input or output name inside a contract quantifier: the passes that rewrite old and outputs match on identifier text, so shadowing can silently change the formula.

  • Pipe-quoted identifiers parse and lower, but the Core formatter does not re-quote every reference, so retained Core text containing them may not re-parse. Prefer regular identifiers when the output must be read back.

The Designer Guide's Planned features section records what is intended for the gaps above and for the To be designed.. sections in this guide.