epfl-lara / stainless

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

Add missing case for Array `typeBounds`, make private final, fix minor bug in `RefinementLifting` #1494

Closed mario-bucev closed 5 months ago

mario-bucev commented 5 months ago

Small PR that addresses 3 minor issues: -Add a missing case for arrays in typeBounds, which would otherwise cause ArrayOfTypeAlias to fail Stainless type-checking -Annotate private methods with xt.Final since these cannot be overridden ("effectively final"). Now PrivateIsFinal passes -Fix a small issue in RefinementLifting that would not properly update the type of each occurrence of variables whose type has been dealiased.