linux v2.4.1 experiment

using mygcc


This directory contains an experiment consisting in applying mygcc to retrieve over 100 already reported bugs in Linux v2.4.1.
These bugs were originally detected using a much more complex, never distributed, C checker called MC, that later evolved as a commercial product. The list of bugs detected by MC is available as an on-line bug database.

To validate mygcc, we chose three checkers used by MC (called NULL, FREE, and BLOCK), rewrote them as constrained reachability properties, and checked 89 among the  concerned C files.


The short story is that mygcc found all the bugs except only 4, introduced only 2 false positives (= false errors), and found 4 new, unknown bugs. This demonstrates that simple reachability properties are sufficient to detect many useful bugs.

You may browse the results, and compare them with MC's database. The results contain one *.check file for each C file that was checked, containing all mygcc messages. Every user-check message contains the name of the C file, the name of the function that failed a user check, and the buggy statement.

Note: As mygcc works on a simplified AST internal to gcc called Gimple, the buggy statement may look different from the source statement, because complex sub-expressions have been replaced by temporary variables. We are working on printing the buggy statement in its original source form.


The contents of the directory is as follows:


To run the tests yourself, you need a Linux/x86 machine. Perform the following steps:

Running the tests will create, for each C file called "f.c", the following files:

After that, you might want to compare your results with the reference results in ref/.
Finally, you might want to erase all the produced files using "make clean".

Last update: 29/8/2008. Contact: