Skip to content

Installation of TChecker

Jump to bottom
Frédéric Herbreteau edited this page Aug 3, 2023 · 19 revisions

Binary distributions can be found from the Releases page. The project TChecker-build-releases provides scripts to build TChecker for Linux/amd64 and Darwin/arm64, as well as a Docker image.

The instructions below are for installation from the sources. Please, notice that these instructions have only been tested on Linux Ubuntu and Mac OS X. The installation instructions below may not work for other operating systems. Please contact us in case of problem.

Requirements

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.12) -- upgrade is comming as CMake < 3.5 will be deprecated
  • flex (>= 2.5.35)
  • bison (>= 3.0.4)
  • The Boost library (>= 1.81.0 -- boost::json is required)
  • Doxygen (>= 1.8.15 -- probably works with earlier versions)
  • Catch2 (>= 3.0.0 -- earlier releases of TChecker only works with v2)

Catch2 can be obtained from Catch2 github repository. Please, refer to Catch2 tutorial for installation instructions. Please, notice that TChecker works with Catch2 v3 from release v0.5. Earlier version of TChecker only works with Catch2 v2.

Building and installing TChecker

We assume that all dependencies have been successfully installed.

Clone the repository:

git clone https://github.com/ticktac-project/tchecker.git

This will create a directory tchecker in the current directory, that contains a fully functional local clone of the project.

Configure the build

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. To that purpose, create a build directory:

mkdir build
cd build

Then, the configuration depends on your system.

Linux users

Run the following command to configure the build:

cmake ../tchecker -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/path/to/install

In the command above, /path/to/install shall be replaced by the desired installation path. Please, refer to Configuration options for details.

In case you elect to build TChecker shared library (see Configuration options below), you shall make the installation directory visible to ld. If you install TChecker in a standard location (e.g. /usr/local), you shall run command ldconfig. Otherwise, you shall add the directory containing libtchecker.so to system variable LD_LIBRARY_PATH.

Mac OS X users

The 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. Mac OS X users will need to install a newer version using MacPorts or Brew (or another packaging system). Then, run the following command to configure the build:

cmake ../tchecker -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=/path/to/install -DCMAKE_PREFIX_PATH=/path/to/bison

In the command above, /path/to/bison shall be replaced by the actual path to the newer bison executable. And /path/to/install shall be replaced by the desired installation path. Please, refer to Configuration options for details.

Configuration options

  • 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 directory local in your account: -DCMAKE_INSTALL_PREFIX=$HOME/local.

  • CMAKE_BUILD_TYPE specifies to build a Debug or a Release version of TChecker. The difference is that the Debug version runs many checks. It is safer but a lot slower. We recommend to build a Release version.

  • set LIBTCHECKER_ENABLE_SHARED to ON in order to build TChecker library as both a static library and a shared library. By default, only the static library is built.

  • if cmake fails to find some of the dependencies, you may need to specify the directories to the software using option CMAKE_PREFIX_PATH and CMAKE_MODULE_PATH.

  • 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 of cmake -h for available generators).

Compilation and installation

The commands below build TChecker and its documentation in the build directory, and then install TChecker in the chosen installation directory (i.e. the directory specified with option CMAKE_INSTALL_PREFIX).

make -j
make doc
make install

The installation procedure creates four directories: bin, lib, include and share/doc/tchecker/html in the installation directory. The TChecker tools 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.

Clone this wiki locally