Mickaël Delahaye


Frama-C/LTest is a generic and integrated toolkit for automation of white-box testing of C programs. Based on Frama-C, this toolkit provides a unified support of many different testing criteria as well as an easy integration of new criteria. It is designed around three basic services (test coverage estimation, automatic test generation, detection of infeasible test requirements) covering all major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Except for the automatic test generation, LTest is available freely under the LGPL 2.1 license.

On this page, we aim to provide LTest's source tarballs and installation instructions.


LTest comes in four modules (LAnnotate, LUncov, LReplay, and LGenTest). Except for LGenTest they are all available for download thereafter. LTest requires a slightly modified version of Frama-C also provided.

Please note that, currently, LTest has only been tested under Linux, though it might work under other Unix systems.





 Benchmark programs

We selected programs to run our experimental evaluation:

 Related publications