Frama-C/LTest

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.

 Downloads

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 )
• Frama-C/LTest
  • LAnnotate : annotates program with labels corresponding to various coverage criteria (DC, CC, MCC, weak mutation, etc.)
  • LUncov : detects infeasible (or uncoverable) labels
  • LReplay : runs tests and collects label coverage data

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

 Installation

Requirements

• OCaml
• GCC
• GNU Make

Steps

• First install the patched Frama-C:

  ./configure
  make
  sudo make install

• Then install each module using the same two commands:

  make
  sudo make install

  Additional information is available in each module in a README file.

 Authors

• Mickaël Delahaye
• Omar Chebaro
• Robin David
• Nikolai Kosmatov
• Sébastien Bardin

 Benchmark programs

We selected programs to run our experimental evaluation:

• Benchmark programs  as in ICST 2014 (see below)
• Updated version  as in TAP 2014

 Related publications

• 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 .