-
Andrei Paskevich authored
On a missing "diverges", Vc emits a warning and adds a "false" sub-goal at the location of the non-terminating loop or function call. The explanation on this sub-goal is "termination", but should probably be "termination (failure)". The "diverges" clase propagates downwards: if it is put on the top-level function, there is no need to repeat it on local functions or abstract blocks.
3e802ac9