The Leak Contradictor is a memory leak detection tool for C programs that proves the lack of memory leaks by disproving their presence. For each heap pointer assignment (called a probe), the tool assumes assumes that the assignment might cause a leak, and then tries to disprove this assumption using a backward dataflow analysis. In many cases, leak probes can be quickly contradicted.
The tool is implemented in the Crystal framework.
Publications
For more information on the algorithm used, please see:
- Memory Leak Analysis by Contradiction
M. Orlovich and R. Rugina,
In Proceedings of the International Static Analysis Symposium (SAS '06)
Seoul, Korea, August 2006.
- A technical report containing the correctness proofs.
Downloads
Download the Leak Contradictor: lc-1.0.tgz.
Note: lc-1.0.tgz includes all of the crystal-1.0 sources.
Installation
Requirements: Java 1.5 and Apache Ant (same as for the Crystal framework).
To install: download the LC distributions, and unzip each
file. Then go to the newly created directory crystal and run ant:
> tar xzf lc-1.0.tgz > cd crystal-1.0 > ant
To run LC, use the shell script "bin/lc". For larger
applications, use the "-h" option of this script to specify larger heap sizes
(the default is 64Mb). For instance, "bin/lc -h 256" runs
crystal with a heap of 256Mb.
Usage
Before running LC, you must generate
preprocessed versions of sources for your application. If you use the gnu
C compiler, this can be done using 'cpp' or 'gcc -E'.
Typically, preprocessed files have extension '.i'.
Then run the LC script on the entire set of preprocessed files:
> bin/lc file1.i file2.i ...
As the program runs, it will output warnings to the standard output, generally giving the location of an allocation statement where the potentially leaked heap cell originated, and the statement where the last reference to the memory is believed to be lost.
At the end, the program will print out a report file "leak-traces.txt"
containing one program trace for each potential bug. Although the tool
builds a set of paths per probe, it randomly picks one for the error report.
Sometimes the chosen path is infeasible, but a very similar execution path
is feasible and does leak memory. Hence, the output report should be used
merely as guidance for manual examination, and not an exact witness for the truth or falsity of the reports.
People
The system is being developed at Cornell University. The current contributors to the project are:
- Maksim Orlovich (maksim at cs cornell edu)
- Radu Rugina (rugina at cs cornell edu)
Feel free to provide us feedback.