Frama-C/LTest

Tool Description

Frama-C/LTest is a toolkit for automated white-box testing of C programs. It was originally created by Mickaël Delahaye and subsequently extended by me. Based on Frama-C, it is designed around three basic services (test coverage estimation, automatic test generation, detection of polluting test objectives) covering all major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. It provides a unified support of many different testing criteria (and also of security hyperproperties) as well as an easy integration of new criteria.

Except for the automatic test generation (based on PathCrawler), LTest is available freely under the LGPL 2.1 license.

Downloads

The installation guide and the first version of LTest can be downloaded from Mickaël's website.

The source code of my newer version of LTest (including hyperlabel support and polluting test objective pruning) can be downloaded here:

  • LAnnotate: hyperlabel annotation module for C code

  • LClean: scalable and robust infeasible and redundant label detection module

  • LReplay: test suite replay and hyperlabel coverage measurement module

Publications

Conceptual and technical details about this newer version of LTest can be found in the following publications: