search

viperproject / gobra

Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
https://gobra.ethz.ch
Other
111 stars 28 forks source link

Cyclic Termination Measures #759

Open ArquintL opened 6 months ago

ArquintL commented 6 months ago

Gobra should reject pure functions that use themselves as a termination measure. While Viper issues a consistency error, Gobra does not.