search

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 when postconditions of pure functions contain old() expressions #1474

Closed zgrannan closed 7 months ago

zgrannan commented 7 months ago

It doesn't make sense to have old() expressions in postconditions of pure functions (since they don't modify the heap). Also, the PureFunctionEncoder can't handle them (resulting in internal/consistency errors).

This PR makes it an error to include old() in postconditions of pure functions. Resolves https://github.com/viperproject/prusti-dev/issues/1306

This PR also includes support for StubFunctionEncoder to handle bodyless functions (e.g. those from #[extern_spec])