Predator

Predator is a practical tool for checking manipulation of dynamic data structures using separation logic. It can be loaded directly into GCC as a plug-in. This way you can easily analyse C code sources, using the existing build system, without any manual preprocessing of them etc. The analysis itself is, however, not ready for complex projects yet. The plug-in is based on Code Listener infrastructure (included). Although the tool is intended to be as portable as GCC is, we support only Linux for now.

News

 SVCOMP'12 — Predator succeeded in the 2012 International Competition on Software Verification!
Predator acquired the gold position in the HeapManipulation category and the silver position in the DeviceDrivers category of the 1st International Competition on Software Verification held at TACAS 2012 in Tallinn, Estonia. If you want to reproduce the competition results, please download the competition candidate and follow the instructions in the file named README-sv-comp-TACAS-2012, which is included in the archive.

 predator-2011-10-11-8a7846b is out!
Predator can now be used to check for error labels reachability, too. It can analyze CIL-generated code with ease. Building Predator from sources is now even more straightforward and user-friendly than ever before. As usually, many bug-fixes and significant performance and memory consumption improvements are included.

Building from Sources (GCC + Predator)

textREADME-fedora
textREADME-ubuntu
curl http://www.fit.vutbr.cz/~idudka/download/predator-2011-10-11-8a7846b.tar.gz \
    | gzip -cd \
    | tar x

cd predator-2011-10-11-8a7846b
make build_gcc
make
make check

Usage

To employ the Predator plug-in in a build of an arbitrary project fully transparently, it is recommended to set certain environment variables. You can use the script register-paths.sh to do this automatically:

. register-paths.sh

Then you can simply use the -fplugin option of GCC as documented in the gcc(1) man page:

gcc -fplugin=libsl.so ...

This will show you the available options of the Predator plug-in itself:

echo please help | gcc -fplugin=libsl.so -fplugin-arg-libsl-help -xc -

Source Code

tgzpredator-2011-10-11-8a7846b.tar.gz
gitgit repository

Documentation

textREADME
pdfPresentation (CAV '11)
linkAPI documentation

Related Papers

  1. K. Dudka, P. Peringer, and T. Vojnar. Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic. In Proc. of 23rd International Conference on Computer Aided Verification - CAV'11, Cliff Lodge, Snowbird, Utah, USA, volume 6806 of LNCS, pages 372--378, 2011. Springer-Verlag.

Authors

Acknowledgement

This work was supported by the Czech Science Foundation (project P103/10/0306), the Czech Ministry of Education (projects COST OC10009 and MSM 0021630528), and the internal BUT FIT project FIT-S-11-1.