search

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 103 forks source link

Termination checks of mutually recursive functions #1443

Open fpoli opened 10 months ago

fpoli commented 10 months ago

@vakaras pointed out that the current encoding of mutually recursive functions might be unsound when the (optional) termination checks are enabled. Until that's fixes, it's up to the users to ensure that all pure function definitions always terminate.