The LIME Concolic Tester for C

The LIME Concolic Tester for C is an automated white-box tester for C programs. Concolic testing is also known as dynamic symbolic execution. It attempts to visit every possible execution path of the program under test.

Releases

• LCT-C-1.0.0.tar.gz
• LCT-C-1.1.0.tar.gz
• LCT-C-1.1.1.tar.gz

Note: The software is only known to work on 64-bit Ubuntu Linux.

Quick-start

• Make sure your installed C++ compiler compiles Clang and LLVM versions 3.1 correctly. Clang version 3.0 is known to work. For a list of compilers that do not compile LLVM correctly see http://llvm.org/docs/GettingStarted.html
• Download the LCT-C-1.1.1 release above and unpack the contents.
• Run make llvm all in the unpacked directory.
• Add the bin subdirectory to your PATH.
• Download Boolector from http://fmv.jku.at/boolector/, compile it, and install the boolector executable into your PATH.
• Download and install the LIME Testbench to get the LIME test server.
• The following steps can be used to automatically test C programs:
  • To use symbolic inputs in the program, use lct_get_int() or the similarly named functions defined in the lct.h file in the lct subdirectory. You will also need to include that file in your source.
  • Compile your C source files with the lct-instr-cc command. It works similarly to a compiler, but you should use the -c and -o flags to produce .o files. This results in instrumented object files.
  • Link your program normally, but include all the .o files from the lct subdirectory, and use -lpthread and -lstdc++ to include the pthread and standard C++ libraries. You can also link in uninstrumented object files, but this may reduce the obtained test coverage.
  • Run the linked program repeatedly on a machine that has the LIME test server running. This should exercise the different execution paths of the program.

Documentation

For more documentation on the LIME tools, see the page for the LIME testbench for Java.

---

Latest update: 22 October 2012.