Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
A Shape Analyzer Based on Symbolic Memory Graphs
C C++ Other

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
build-aux
cl
docs
fa
fwnull
include
sl
tests
.gitignore
COPYING
Makefile
README
README-sv-comp-TACAS-2012
switch-host-gcc.sh

README

Predator and Forester
=====================
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 Predator is intended to be as
portable as GCC is, we support only Linux for now.  You can find the latest news
on the following project page:

    http://www.fit.vutbr.cz/research/groups/verifit/tools/predator

Forester is an experimental tool for checking manipulation of dynamic data
structures using *forest automata*.  As in case of Predator, it can be loaded
directly into *GCC* as a *plug-in* to analyse C code sources.  However, the analysis
itself is not yet mature enough to be able to verify ordinary programs.  Although
Forester is intended to be as portable as GCC is, we support only Linux for now.
You can find the latest news on the following project page:

    http://www.fit.vutbr.cz/research/groups/verifit/tools/forester

Predator, Code Listener, and Forester are licensed as GPLv3+, see COPYING for details.

Building from sources against a local build of GCC [recommended for end users]
==============================================================================

(1) Install all dependences of GCC
----------------------------------
   * GMP library
     - available at http://gmplib.org/
     - package is usually called 'gmp'
     - on binary distros you may need also the 'gmp-devel' sub-package

   * MPC library
     - available at http://www.multiprecision.org/
     - package is usually called 'mpc' or 'libmpc'
     - on binary distros you may need also the 'libmpc-devel' sub-package

   * MPFR library
     - available at http://www.mpfr.org/
     - package is usually called 'mpfr'
     - on binary distros you may need also the 'mpfr-devel' sub-package

(2) Install all dependences of Predator and Forester
----------------------------------------------------
   * CMake 2.8+
     - available at http://www.cmake.org
     - the executable is called 'cmake'
     - usually provided by a package called 'cmake'
     - though minimal required version of CMake is 2.6, known to work is 2.8+,
       please report any issues with other CMake versions

   * Boost libraries 1.37+
     - available at http://www.boost.org/
     - package is usually called 'boost'
     - on binary distros you may need also the 'boost-devel' sub-package
     - if you are not able to install a new enough version of Boost on your
       system, try to unpack a local instance of it by typing 'make build_boost'

   * 32bit system headers, especially in case of 64bit OS
     - on Ubuntu/Debian provided by a package called 'libc6-dev-i386'
     - you can try to check their presence
       by 'gcc -m32 -o /dev/null /usr/include/stdlib.h'

(3) Build the GCC compiler from sources
---------------------------------------
This step requires approximately 2 GB of free disk space.  The following command
downloads the sources of a stable GCC release, builds them in a minimalistic way
and install them into a local directory:

    make build_gcc

The above step is the most time-consuming step, which can take from 5 minutes to
several hours, depending on your network bandwidth, machine performance and the
current load of the machine.  The download step can be accelerated by selecting
a closer mirror to download GCC from.  The build step can be accelerated by
giving the option '-jN' to 'make', where N is the number of CPU cores plus one
(a commonly used heuristic, there exist several others).  But first make sure
that your machine has enough resources for building GCC in parallel.

(4) Build Code Listener, Predator and Forester from sources
-----------------------------------------------------------
The following command builds Code Listener, Predator and Forester from sources:

    make

Again, the build can be accelerated using the '-j' option of 'make', as stated
above.  After a successful build of Predator (or Forester), it is suggested (but
not required) to run the test-suite shipped with Predator (or Forester) to ensure
the plug-in works as the authors intended to.  The test-suite for Predator consists
of more than 200 regression tests that can be run using the following command:

    make check

As well as the build, the test-suite can run in parallel in order to boost the
performance.  Now the '-jN' parameter needs to go to 'ctest' instead of make:

    make check CTEST="ctest -j9"

(5) Prepare environment for running Predator transparently [optional]
---------------------------------------------------------------------
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.

    . sl_build/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 -


(6) Prepare environment for running Forester transparently [optional]
---------------------------------------------------------------------
Analogically to Predator you can also set up the environment for Forester by
running the following script:

    . fa_build/register-paths.sh

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

    gcc -fplugin=libfa.so ...

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

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

Building from sources against the system GCC
============================================
This method requires a build of GCC with plug-in support compiled in (not
necessarily the system one).  The currently supported version of GCC is 4.7.1
and the test-suite is guaranteed to fully succeed only against this version of
GCC.  However, the Predator plug-in itself is known to work with GCC 4.5.x and
GCC 4.6.x equally well.

You can use the 'switch-host-gcc.sh' script to rebuild Code Listener, Predator,
and Forester against a GCC build of your choice.  For details, please run
'switch-host-gcc.sh' without any arguments.  The script needs to be run in the
same directory as this README is.  If it fails, make sure your environment is
sane.  Especially check the PATH and LD_LIBRARY_PATH environment variables.
Something went wrong with that request. Please try again.