-
Notifications
You must be signed in to change notification settings - Fork 17
Installation of TChecker
Please, notice that TChecker has only been tested on Linux and Mac OS X. The installation instructions below may not work for other operating systems.
TChecker depends on several softwares and libraries listed below. Linux users can install most softwares using the packaging system shipped along with their distribution. Mac OS X users can install the required software using an external packaging system like Brew or MacPorts.
- a C++ compiler with decent C++17 support (Clang >= 3.6 or GNU g++ >= 6 should work. Apple LLVM >= 10.0.0 works)
- CMake (>= 2.8)
- flex (>= 2.5.35)
- bison (>= 3.0.4)
- The Boost library (>= 1.65.0 -- probably works with earlier versions)
- Doxygen (>= 1.8.15 -- probably works with earlier versions)
- Catch2 (>= 2.7.0)
Catch2 can be obtained from Catch2 github repository. Please, refer to Catch2 tutorial for installation instructions.
We assume that all dependencies have been successfully installed.
git clone https://github.com/fredher/tchecker.git
This will create a directory tchecker
in the current directory, that contains a fully functional local git repository of the project.
We use cmake
to build the project. We recommend to build TChecker out of the source directory. This allows to easily remove the files generated by cmake
and by the compiler. This also allows cmake
to build a project for your favorite IDE out of the source directory.
The following command runs cmake
to create a build
directory containing all files required to compile TChecker from the source in directory tchecker
.
cmake -Bbuild -Stchecker -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/path/to/install
This command should be launched from the current directory. It creates a new directory build
, hence, current directory contains tchecker/
and build/
. Several options shall be specified to cmake
, in particular:
-
CMAKE_INSTALL_PREFIX
specifies the path where TChecker shall be installed. Default directory is/usr/local
. You may need administrator privileges to write into/usr/local
. Hence, it may be relevant to install TChecker in your account. For instance, to install in directorylocal
in your account:-DCMAKE_INSTALL_PREFIX=$HOME/local
. -
CMAKE_BUILD_TYPE
specifies to build aDebug
or aRelease
version of TChecker. The difference is that theDebug
version runs many checks. It is safer but a lot slower. We recommend to build aRelease
version. -
if
cmake
fails to find some of the dependencies, you may need to specify the directories to the software using optionCMAKE_PREFIX_PATH
andCMAKE_MODULE_PATH
.-
Mac OS X users: the default version of bison that is shipped with Apple development tools is quite old, and it does not support some of the features required by TChecker. You will need to install a newer version using MacPorts or Brew (or another packaging system). Then, you will need to specify the path to the new
bison
binary adding-DCMAKE_PREFIX_PATH=/usr/local/opt/bison/bin
to the command above (the exact path depends your system). -
Linux users: you will need to install the package
libboost-all-dev
, butcmake
will not be able to find it. You will need to specify the path tocmake
adding-DCMAKE_MODULE_PATH=/usr/share/cmake-3.10/Modules
to the command above (the exact path depends on your system).
-
-
you may build a project for you favorite IDE adding option
-G my_ide
to the command above (my_ide
should be replaced by your favorite IDE, see the output ofcmake -h
for available generators).
The command below builds TChecker in the build
directory and installs it in the chosen directory (i.e. the directory specified with option CMAKE_INSTALL_PREFIX
).
cmake --build build/ --target install
Option -j N
can be added to the command above to use parallel build with N
parallel jobs.
The installation procedure creates four directories: bin
, lib
, include
and share/doc/tchecker/html
in the installation directory. The TChecker tool can be found in directory bin
(see Using TChecker). The development tools are provided in the other directories: the
headers in include
, the library in lib
, and the Doxygen documentation in share/doc/tchecker/html
.