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.


./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.

Adding the option --enable ana.context.widen will enable widening on the contexts in which functions are analyzed. This avoids stack overflows possibly caused by the analysis of recursive functions.

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


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


  1. Doesn't properly escape -D argument values (,
  2. Errors with .deps and Makefile targets (
    • Workaround is to remove the manually.
  3. Assumes English locale (GobCon 23.02.2022 notes).
  4. Doesn't completely decompose multi-file targets (
  5. Uses relative paths for preprocessing and thus in AST.


  1. Bear 2.3.11 from Ubuntu 18.04 produces incomplete database (,
    • Bear 3.0.8 seems fine.


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