Debugging C0 Programs

This page collects some hints and advice on debugging C0 programs. Soon, some examples will be added here; for now there are just some brief words of advice.

There are several types of errors that can arise in C0 programs. First, there are the static errors which arise before your program is ever executed.

• Lexical errors, like 0a4 which is not a legal number of identifier.
• Syntax errors, like f(,3) which is not a legal function call.
• Type errors, like true != 3 which attempts to compare a boolean and an integer.

Next are the dynamic errors which arise during execution.

• Runtime errors, like 1 / 0 which raises an exception.
• Contract errors, like f(-1) if f requires it argument to be positive.
• Logical errors, where the program does not abort but does not give the right answer.

No matter what you suspect your bug is, you should always use the -d flag to enable dynamic checking unless it makes the program too slow to exhibit the problem.

## Debugging with Contracts

First we have to agree that runtime errors, like 1 / 0 should never arise in a correct program. This is absolutely central. Expressions which raise runtime errors in C0 will have undefined behavior in C and therefore have to be avoided at all cost. It is expressions with undefined behavior that are exploited by viruses and other malware that may infect your computer.

Contract errors are a bit different. While they also abort the program, they are sometimes required! For example, a correct implementation of sort(int[] A, int n); (sort the array segment A[0..n)) should signal a contract violation if it is called with a negative n.

Recall that to check contracts, you must compile code with the -d flag. Also remember that contracts are only checked when they are reached during program execution, so good coverage in test cases is still important with contracts.

The types of runtime errors in C0 are:

• Division by 0, as in 1/0. This prints Floating exception, even though no floating point numbers are involved. You should find divisions a/b and reason whether b might be 0. Use functions' pre- and post-conditions, loop invariants, and other assertions you already have. If you are not sure add a contract //@assert b != 0; somewhere before the division to check. Now the error message will report a file and line number of the assertion that failed (for example, assert-div0.c0:3.3-3.16: assert failed) and Abort to indicate a failure of contracts.
• Array reference out of bounds, as in A[-1]. This prints Out of bounds array access and Segmentation fault. You should find array access A[e] and reason how it might be out of bounds. If you are not sure, guard the access with a contract //@assert 0 <= e && e < \length(A);. Now the error message will report a file and line number of the assertion that failed.
• Null pointer dereference, as in **alloc(int*); This print attempt to dereference null pointer and Segmentation fault. You should find pointer dereferences (either p->f or *p) and reason whether p might be null. If you are not sure add a contract //@assert p != NULL;. Now the error message will report a file and line number of the assertion that failed.

In each case we can add assertions (or other contracts) to close in on the location and course of the runtime error.

## Debugging with Print Statements

Sometimes it is helpful to see the values of variables, or verify that certain places in the code have been reached. For this, you should include `#use ' at the beginning of the file and then add print statements in strategic places in your function.

But beware! Output in C0 (like C and some other languages) may be buffered, which means that the output to the console does not take place immediately, but only when a line of output is complete. So you should always add newlines (as in print("Got here!\n");) or print newlines by themselves (as in print("i = "); printint(i); print("\n");).

If you forget the newline character, \n in strings, then the string may never show and you may be misled as to whether certain places in the code are reached!