Capturing standard output in counterexample traces

[michael-emmi]

Counterexample traces can be hard to reason about, since we see only a limited view of the program values along a given path. Ideally, wouldn’t it be great to fire up a debug session, as if we were using gdb, lldb, etc, but with Boogie as the underlying runtime? This would seem to require a fair amount of effort to implement :-)

In the mean time, wouldn’t it be great to support the popular printf debugging style?

For instance the counterexample trace of this program

#include <smack.h>
#include <stdio.h>

int main() {
	int x = 1;
	printf("value: %d", x - 1);
	assert(x - 1);
}

could include the output

value: 0

As a first step, we could trying handling printf only, and then work our way up to capturing other output functions.

Note that besides helping ad-hoc verification debug sessions, this would allow users to reuse existing logging/debugging mechanisms already in their code.

[michael-emmi]

^ @nchong-at-aws