Help

Command-line Options

To list all available options, run frama-c -plugin-h, where plugin is either deadlock or racer. As for other Frama-C plugins, are options are of form -plugin-option. Boolean options can be set by -plugin-option and turned off by -plugin-no-option.

Options common for both plugins

• -plugin-use-eva: Plugin will run value analysis provided by EVA and use its result. This option may increase precision, but the running time may be significantly longer.

• -plugin-out-json path: Store information about analysis to the json file given by path.

General Options

Since Racer uses results of lockset analysis computed by Deadlock, the following options will affect the behaviour of both plugins:

• deadlock-callstack-mode <none | calls | branching>: How to print callstacks in reports:

  • calls: Only entry points and calls are printed.
  • branching: In addition, branches taken at conditions are also printed.

• -deadlock-conc-model <model | path> : Allows to customise concurrency model (locking functions, thread-creating functions, ...). Can be either given by a json file (see an example) or one of predefined models can be used - currently pthread (default) and c11_threads are available.

Deadlock detection options

• -deadlock-conc-check: Use heuristics to check whether detected deadlocks can really happen in some parallel execution (set by default).

• -deadlock-ignore-self-deadlocks: Ignore deadlocks caused by a single thread that tries to acquire a lock which it already owns (set by default, because those are often false alarms).