Stack overflow errors ought to be caught

[nickbattle]

Currently, stack overflow problems - usually caused by recursive loops, often implicitly via invariants that reference themselves - are not caught by the Overture runtime and simply drop out to the Java default exception handling. This dumps the Java stack to the console, but that is not helpful from a modelling perspective since it does not include the names of VDM variables and functions.

Handling stack overflows in Java is difficult because when they occur, by definition, you do not have very much stack available to handle the error! The trick is to pop a certain number of frames off the stack, while still handling the exception, and then process the remaining VDM stack with a minimum of new Java frame usage (ie. not recursing!). This is reasonable since, if you have broken the stack limit, you are probably in a recursive loop anyway and the remaining frames on the stack will be enough to identify the loop problem, even if strictly they were not the top of the stack when the limit was reached.

Experiments seem to verify that this approach is workable. It is certainly better than letting Java crash. Pushing this change to ncb/development for further testing.

[nickbattle]

Now available in ncb/development.

[nickbattle]

Pushed a slightly enhanced fix, which doesn't produce multiple stack dumps on the console.

[nickbattle]

Pushed another small tweak to make a more sensible trim of the stack dump. It now prints the top 50 frames, which should be enough to identify any looping, and an indication of how many frames were skipped, followed by the last 5 frames to give you some idea of the root of the problem.