Rob,
Rob Arthan wrote:
David,
On Wednesday 21 Jul 2004 3:47 pm, David Matthews wrote:
Rob,
Rob Arthan wrote:
... Unfortunately PolyML.exception_trace almost never gives me useful results. I think this maybe because I'm nearly always executing code via PolyML.compiler. Does that sound right? And is there a work-around?
The most likely reason is that the function that is raising the exception has been inserted inline into a calling function. This can happen through several levels so it may not be obvious which source function raised the exception. You can try reducing PolyML.Compiler.maxInlineSize and recompiling. ...
How about the following?
(**** ML BEGINS ****) PolyML.Compiler.maxInlineSize := 0;
fun g1 () : int = ( raise Div );
fun g2 () = ( g1 () );
fun g3 () = ( g2() );
fun g4() = ( g3() );
PolyML.exception_trace g4; (**** ML ENDS ****)
Even if I run this on the ML compiler database (i.e., without any of my ProofPower code in the way), I get an empty stack trace.
Yes, thanks for pointing this out. That's another reason for missing entries in the stack trace: tail recursion removal. The exception trace is simply the return entries on the stack. In this case the functions are tail-recursive so the function calls are implemented as jumps, leaving nothing on the return stack. If you replace the functions by multiple calls, e.g. fun g2 () = ( g1 (); g1() ); then you will get the trace:
Exception trace for exception - Div g2(1) g3(1) g4(1) End of trace
Whether all this makes the exception trace useless or not depends a lot on your coding style.
The idea of PolyML.exception_trace is that it can provide a trace without any impact on the run-time performance of the program, apart from a very small overhead to set up the trace. In contrast, turning on the debugging option in the compiler can add a very significant overhead.
Regards, David.