Add custom location marks to exception backtraces

[sim642]

Problem

In 023b7c1, current_loc was explicitly added back to the "About to crash" error. Actually Messages.error already uses current_node unless specified otherwise. That's why in #533 I removed the explicit location specification.

But that error didn't have a location (from a node) because there is no current node at that point. Some current_loc is always present, so it seems like that works on the "About to crash" error, but it actually doesn't.

Even when an exception is raised in a transfer function, using current_loc for "About to crash" just gives it the last global variable definition location! That is because it is set by the simulated global initializer transfer functions:

analyzer/src/framework/control.ml

Lines 276 to 280 in 4828e7b

	let transfer_func (st : Spec.D.t) (loc, edge) : Spec.D.t =
	if M.tracing then M.trace "con" "Initializer %a\n" CilType.Location.pretty loc;
	(*incr count;
	if (get_bool "dbg.verbose")&& (!count mod 1000 = 0) then Printf.printf "%d %!" !count; *)
	Tracing.current_loc := loc;

But unlike actual transfer functions, this forgets to unset the current location after calling Spec.assign and thus the last global initializer location simply leaks to the rest.

Therefore, current_loc for "About to crash" is plain incorrect and even misleading.

Solution

This PR proposes a solution to the above problem by allowing raised exceptions to be marked with some custom data.

Arbitrary custom data can be added and a printer for it registered (just like exceptions themselves). An exception handler can then add such custom mark to the exception as it is reraised.
In this particular case, this is done in FromSpec, where we manage current_loc during actual transfer function evaluation.

Uncaught exception printing is extended to also print all the marks added to the exception. The marks actually stack, so you don't just get the innermost current_loc for where the exception occurred, but the entire stack of current_locs, which is analogous to the entire stack of OCaml transfer function calls.
In case -v is not used, the first mark is also added to the "About to crash" error.

[michael-schwarz]

Nice catch!