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 support for exported methods #1501

Closed mario-bucev closed 4 months ago

mario-bucev commented 5 months ago

The Scala compiler generates a forwarder for each exported method, however the preconditions are not taken into account, which means the forwarder will be invalid. The idea is to drop these forwarded method and "de-alias" the symbol to get the original method or field.