RacerF and DeadlockF are static analysers for detection of data races and deadlocks in multi-threaded C programs with mutexes. Both tools are implemented as plugins of the Frama-C platform.
The recent versions of the plugins are compatible with Frama-C 29.0 (Copper).
For installation, opam package manager and OCaml >= 5.1 is necessary. After cloning this repository, run opam install .
The simplest way to run the plugins is:
frama-c -racer source_file1.c source_file2.c ...
frama-c -deadlock source_file1.c source_file2.c ...
Several commandline options can be specified. The options related to a specific plugin are prefixed -racer and -deadlock, respectively, the general options are prefixed by -cc.
Run `frama-c [racer|deadlock]-h to see more details.
The script racerf.py can be used to run RacerF using a combination of under- and over-approximating strategy as follows:
./scripts/racerf.py -machdep=[gcc_x86_32|gcc_x86_64] [--under|--over] [--debug] [frama-c-options] source_file.c
The options --under and --over run just under- and --over approximation respectively.
By default, the combined strategy is used.
Currently only single source file can be analysed using the wrapper.
Moreover, machine model of Frama-C needs to be one of gcc_x86_32 or gcc_x86_64.
-
Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code. ECOOP 2025.
-
Tomáš Dacík and Tomáš Vojnar. RacerF: Data Race Detection with Frama-C (Competition Contribution). SV-COMP 2025.
-
Tomáš Dacík. Static Analysis in the Frama-C Environment Focused on Deadlock Detection. Bachelor's Thesis. Brno University of Technoloy. 2020. Supervised by Tomáš Vojnar.
If you have any questions, do not hesitate to contact the tool/method authors:
The plugin is available under MIT license.