Running Goblint

Basic Execution

To analyze a C-source file with Goblint, you may simply pass the path to the file as a command line argument to it. To generate an HTML-output that can be inspected using the browser, additionally pass the --html flag.

Example:

./goblint tests/regression/01-cpa/02-branch.c --html

Passing Options

Goblint offers many options to tweak how the analysis is performed. For more information on how to set options, run:

./goblint --help

For a list of all options and their possible configurations, run:

./goblint --print_all_options

To use one of the pre-defined configurations, run:

./goblint --conf path/to/config.json files

Analyzing Recursive Programs

In some cases, when using the default configuration, Goblint might not terminate in reasonable time on recursive programs, or crash in a stack overflow (indicated by the error message exception Stack overflow). If the stack overflow occurs within a C function called by Goblint, it will result in the following error message: Command terminated by signal 11.

The recommended way to handle this is to use context gas (Erhard et al., 2024), which limits the number of context-sensitive function calls in a call stack. Any calls beyond the limit are analyzed context-insensitively (with an empty context). Setting the option --set ana.context.gas_value N enables context gas for non-negative values of N. A higher value of N gives a more precise analysis, while a lower value reduces the risk of stack overflows and non-termination. A value of 30 is a good starting point. Negative values disable context gas, and 0 makes the analysis context-insensitive.

Alternatively, adding the option --enable ana.context.widen will enable widening on the contexts in which functions are analyzed, which also avoids stack overflows possibly caused by the analysis of recursive functions, but is relatively more expensive.

Project analysis

To analyze real-world projects, Compilation Databases can be used. First, generate a compilation database compile_commands.json:

  • For CMake projects, add -DCMAKE_EXPORT_COMPILE_COMMANDS=ON argument to cmake.
  • For Make projects:
    • Use Bear: bear -- make (preferred).
    • Or use compiledb: compiledb make.

Second, run Goblint on the compilation database:

goblint compile_commands.json

Caveats

Here is a list of issues and workarounds for different compilation database generators we have encounted.

compiledb

  1. Doesn't properly escape -D argument values (https://github.com/goblint/bench/issues/8#issuecomment-1017538298, https://github.com/goblint/bench/issues/14#issue-1112574635).
  2. Errors with .deps and Makefile targets (https://github.com/goblint/bench/issues/17).
    • Workaround is to remove the manually.
  3. Assumes English locale (GobCon 23.02.2022 notes).
  4. Doesn't completely decompose multi-file targets (https://github.com/goblint/analyzer/issues/624#issuecomment-1060566770).
  5. Uses relative paths for preprocessing and thus in AST.

bear

  1. Bear 2.3.11 from Ubuntu 18.04 produces incomplete database (https://github.com/goblint/bench/issues/7#issuecomment-1011055984, https://github.com/goblint/bench/issues/7#issuecomment-1011987188).
    • Bear 3.0.8 seems fine.

SV-COMP

The most up-to-date SV-COMP configuration is in conf/svcomp.json. There are also per-year configurations (e.g. conf/svcomp24.json) which try to reflect that year's submission using current option names. Due to unconfigurable changes (e.g. bug fixes) these do not exactly behave as that year's submission. See SV-COMP submissions in GitHub releases for exact submitted versions.

In SV-COMP Goblint is run as follows:

./goblint --conf conf/svcomp.json --set ana.specification property.prp --set exp.architecture {32bit,64bit} input.c

Goblint YAML correctness witness validator is run as:

./goblint --conf conf/svcomp.json --set ana.specification property.prp --set exp.architecture {32bit,64bit} --set witness.yaml.unassume witness.yml --set witness.yaml.validate witness.yml input.c