Termination checks for functions and methods

[fpoli]

Viper (the underlaying verification language) has termination checks but Prusti doesn't use them yet.

• [x] The user documentation should at least make it clear that at the moment one can derive false by writing pure functions that don't terminate.
• [ ] Implement termination checks for pure functions.
• [ ] Implement termination checks for methods.