Forbidding function self-references in postconditions for functions without decreases clauses

[marcoeilers]

Replaces PR #669.
As discussed with Peter and Alex, we

• forbid references to the function itself (and functions it calls in a mutual recursion cycle) in its postcondition
• unless the function has a decreases clause
• for both abstract and non-abstract functions.

The intended effect is to prevent potentially unsound reasoning caused by self-references (see issues #668 and #525), which is surprising for many users. Now, when using such self-references, user are forced to either prove termination using decreases clauses (in which case our function encoding is sound), or make explicit that they are assuming termination or accepting that the function might not terminate (writing decreases _ or decreases *).

This new check is implemented in beforeVerify in the termination plugin, since it checks for the presence of decreases-clauses and therefore would not work without the termination plugin. That also means that frontends will not be affected by this change by default, unless they choose to invoke the termination plugin explicitly.

The errors are reported as consistency errors and distinguish between the kind of function call:

• "Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Use "result" instead to refer to the result of the function." for self-references with the functions arguments, i.e., self-references that can be replaces by result.
• "Function ${f.name} has a self-reference in its postcondition and must be proven to be well-founded. Add a "decreases" clause to prove well-foundedness." for self-references with different arguments.
• "Function ${f.name} has a call to mutually-recursive function ${calledFunc.name} in its postcondition and must be proven to be well-founded. Add a "decreases" clause to prove well-foundedness." otherwise.

[ArquintL]

looks good to me, I only have one smaller comment