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
.
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 tocmake
. - For Make projects:
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¶
- 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). - Errors with
.deps
and Makefile targets (https://github.com/goblint/bench/issues/17).- Workaround is to remove the manually.
- Assumes English locale (GobCon 23.02.2022 notes).
- Doesn't completely decompose multi-file targets (https://github.com/goblint/analyzer/issues/624#issuecomment-1060566770).
- Uses relative paths for preprocessing and thus in AST.
bear¶
- 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