Raise an error if old() expressions are used in local vars outside of loops

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.

http://prusti.org

Other

1.52k stars 102 forks source link

Raise an error if old() expressions are used in local vars outside of loops #1482

Closed zgrannan closed 6 months ago

zgrannan commented 6 months ago

If an expression old(E) is used within an assert statement, and E contains a local variable, then the fold-unfold algorithm will raise an error. This PR changes Prusti to detect such patterns and present a user-friendly error instead.