Doomed Program Points
The main idea behind this work is to create an error detection tool that only informs the user about statements that will always fail when executed. This means that the tool will never come up with a false positive. It only fires if there is a statement in the program that cannot be executed without creating an error. We call this approach sound error detection.
A program point is doomed if there is no execution passing it that terminates normally. This does not mean that the program will always crash. It means, that, e.g. there is a statement in a certain branch that is never executed on a terminating execution.
Example 1
int a[10];
for ( int i=0; i<=10; i++) a[i] =i;
The loop will never terminate normally because there is always an out-of-bounds error in the last iteration. This means that the last iteration of the loop has no admissible execution and thus is doomed.
Our tool will report the break and increment operation of the for-loop and the array access as witnesses for the doomed program point.
Note that our approach does not care about termination it only states that the last iteration has no admissible execution.
Example 2
if (c) {
p=NULL;
}
*p = 5;
Any execution passing p=NULL will crash when p is dereferenced. Thus, the assignment p=NULL is doomed according to our definition. Our tool will report both statements p=NULL and *p=5 because both are needed to prove that p=NULL is doomed.
Detecting Doomed Program Points
- Download Boogie
- Write a Boogie Program or generate one using Spec# or VCC
- Run Boogie.exe /vc:doomed myfile.bpl
- Give us Feedback