Fix issue #841

[jcp19]

This PR fixes issue #841 and applies the following changes:

• unifies the logic to check the signature/contract of pure functions between in interface declarations and outside of it
• it moves the checks of well foundedness of termination measures from MemberTyping.scala to GhostMemberTyping.scala
• it disallows conditional termination measures in ghost or pure functions/methods. We currently do not check that they are exhaustive, and given that this feature is pretty much never used, I went with the simple syntactic check instead of a sematnic one, which is more efficient

[ArquintL]

Looks overall good to me but I've left some requests for small changes

[ArquintL]

Suggested change

	// (João) Conditional termination measures are a very rarely used feature. They allow defining termination measures
	// case-per-case. However, for pure or ghost functions and methods, we need to show that all conditions provided
	// (João) Conditional termination measures are a very rarely used feature. They allow defining termination measures
	// case-by-case. However, for pure or ghost functions and methods, we need to show that all conditions provided

[ArquintL]

Suggested change

	case Some(n) => error(n, "Conditional termination measures are not allowed in pure members.")
	case Some(n) => error(n, "Conditional termination measures are not allowed for pure or ghost functions and methods.")

[ArquintL]

this if condition is redundant

[ArquintL]

this if condition is redundant

[ArquintL]

three comments:

• can we change the behavior such that this function can be called for any spec and internally checks whether it's a spec for a ghost or pure function / method? That's the intuition I have for these wellFoundedIf... functions. Alternatively, please add a require stmt that checks this assumption
• Maybe I'm missing something but isn't this function only called for explicitly ghost functions and methods? To me, it seems like we do not call this function for actual pure functions and methods
• can we rename this function? Without looking at its implementation, I do not have any clue what Needed is supposed to do. What about wellFoundedIfGhostOrPure?

[ArquintL]

Suggested change

	//:: ExpectedOutput(type_error)
	decreases _ if b
	//:: ExpectedOutput(type_error)
	decreases _ if b // we syntactically disallow conditional termination measures for members that must terminate

[ArquintL]

I'd split the errors into separate interface functions. Furthermore, I find it a bit funny that one error occurs at the pure keyword whereas the other errors occur at the parameter declaration site but that's just an artifact of how we type-check. We could consider making the following declarations one-liners such that the testcases are not overly restrictive (should we ever indicate missing termination measures, e.g., at the function name

Suggested change

	// Type error, pure function does not have termination measures.
	//:: ExpectedOutput(type_error)
	pure
	// Type error, pure function cannot have variadic parameters.
	//:: ExpectedOutput(type_error)
	M(a ...int) int
	// Type error, pure function does not have termination measures.
	//:: ExpectedOutput(type_error)
	pure
	M1(a int) int
	// Type error, we do not permit conditional termination measures for members that must terminate
	//:: ExpectedOutput(type_error)
	decreases if a == 42
	pure
	M2(a int) int
	decreases
	pure
	// Type error, pure function cannot have variadic parameters.
	//:: ExpectedOutput(type_error)
	M3(a ...int) int
	decreases
	pure
	// Type error, pure function must have exactly one return parameter
	//:: ExpectedOutput(type_error)
	M4(a int)