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.
- Patched version of Frama-C Neon (or if you prefer just the patch )
Please note that, currently, LTest has only been tested under Linux, though it might work under other Unix systems.
- GNU Make
- First install the patched Frama-C:
./configure make sudo make install
- Then install each module using the same two commands:
Additional information is available in each module in a README file.
make sudo make install
- Mickaël Delahaye
- Omar Chebaro
- Robin David
- Nikolai Kosmatov
- Sébastien Bardin
Benchmark programsWe selected programs to run our experimental evaluation:
- Benchmark programs as in ICST 2014 (see below)
- Updated version as in TAP 2014
- Sébastien Bardin, Nikolai Kosmatov and François Cheynier, “Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria”, in the 7th IEEE International Conference on Software Testing, Verification and Validation (ICST), Cleveland, Ohio, USA, April 2014. IEEE. Author copy .
- Sébastien Bardin, Omar Chebaro, Mickaël Delahaye and Nikolai Kosmatov, “An All-in-One Toolkit for Automated White-Box Testing”, in the 8th International Conference on Tests and Proofs (TAP), York, UK, July 2014. Springer. Authors' extended version .
- Sébastien Bardin, Robin David, Mickaël Delahaye, Nikolai Kosmatov, Mike Papadakis, Yves Le Traon and Jean-Yves Marion, “Sound and Quasi-Complete Detection of Infeasible Test Requirements”, in the 8th International Conference onSoftware Testing, Verification and Validation (ICST). IEEE. To appear. Authors' extended version .