0db: A Static Debugger for C
A static debugger is the compile-time analogue of runtime debuggers like GDB. Runtime debuggers require you to execute a program in order to analyse it, but 0db shows line-by-line the state of a C program on the basis of the semantics of the language alone. This matters because at runtime we interact with a very tiny subset of a program’s possible behaviours. In the state supplied by 0db you see at once what applies to all possible executions of a program.
0db is an interface for Xr0, a new verifier meant to eliminate undefined behaviour from C. Thus 0db is, of necessity, as limited as Xr0, which works for a small-but-growing subset of C89. Its main utility right now is it helps us debug Xr0, because it provides a human-understandable interface for the verification process. So although it may not be ready to help you debug your C programs, it shows what Xr0 is and can become: that is, we hope, it shows something new of what programming is and can be.
Try it
You can try 0db here.
Examples
0db gives you a way to control and view Xr0’s motion through your program. We’ve broken down a couple of examples to help explain what it shows. The first is more an in medias res showcase than a bona fide walk-through like the second.