Fix filtering for `while` loops and inner functions - Githubissues

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

Fix filtering for `while` loops and inner functions #1471

Closed mario-bucev closed 9 months ago

mario-bucev commented 9 months ago

This changes how --functions filters functions in presence of while loops and inner functions.

Loops: when a function is specified in --functions, all its while functions get verified as well
Inner function: if a function containing inner functions is passed to --functions, all its inner functions get verified as well. It is also now possible to verify an inner function without verifying its parent function.

Note: most of the diffs are from merging the test config files for the equivalence checking component due to a test suite refactor.

mario-bucev commented 9 months ago

Requires https://github.com/epfl-lara/stainless/pull/1472 to be merged first