epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 50 forks source link

Relax `isExpressionFresh` and improve aliasing error messages #1468

Closed mario-bucev closed 9 months ago

mario-bucev commented 9 months ago

Relax the condition over which an expression is considered to be "fresh" to include bindings of match expression and seeing through non-recursive function. It also changes the rule for Let for which I'm not so sure about: Before: Let(vd, e, b) expression fresh iff e is fresh and b as well, where we consider vd as fresh when recurring on b Now: Let(vd, e, b) fresh iff b is fresh, where we add vd as a fresh binding when recurring on b provided e is fresh. These changes allows to accept FreshExpr.scala (which was rejected before).

It also improves a bit the "illegal aliasing" error messages.