Type: object
No Additional Properties

files

Type: array of string Default: []

Files to analyze.

No Additional Items

Each item of this array must be:

Type: string

outfile

Type: string Default: ""

File to print output to.

justcil

Type: boolean Default: false

Just parse and output the CIL.

justcfg

Type: boolean Default: false

Only output the CFG in cfg.dot .

verify

Type: boolean Default: true

Verify that the solver reached a post-fixpoint. Beware that disabling this also disables output of warnings since post-processing of the results is done in the verification phase!

mainfun

Type: array of string Default: ["main"]

Sets the name of the main functions.

No Additional Items

Each item of this array must be:

Type: string

exitfun

Type: array of string Default: []

Sets the name of the cleanup functions.

No Additional Items

Each item of this array must be:

Type: string

otherfun

Type: array of string Default: []

Sets the name of other functions.

No Additional Items

Each item of this array must be:

Type: string

allglobs

Type: boolean Default: false

Prints access information about all globals, not just races.

kernel

Type: boolean Default: false

For analyzing Linux Device Drivers.

dump_globs

Type: boolean Default: false

Print out the global invariant.

result

Type: enum (of string) Default: "none"

Result style: none, fast_xml, json, pretty, json-messages, sarif.

Must be one of:

  • "none"
  • "fast_xml"
  • "json"
  • "pretty"
  • "json-messages"
  • "sarif"

solver

Type: string Default: "td3"

Picks the solver.

comparesolver

Type: string Default: ""

Picks another solver for comparison.

allfuns

Type: boolean Default: false

Analyzes all the functions (not just beginning from main). This requires exp.earlyglobs!

nonstatic

Type: boolean Default: false

Analyzes all non-static functions.

colors

Type: enum (of string) Default: "auto"

Colored output (via ANSI escape codes). 'auto': enabled if stdout is a terminal (instead of a pipe); 'always', 'never'.

Must be one of:

  • "auto"
  • "always"
  • "never"

g2html

Type: boolean Default: false

Run g2html.jar on the generated xml.

save_run

Type: string Default: ""

Save the result of the solver, the current configuration and meta-data about the run to this directory (if set). The data can then be loaded (without solving again) to do post-processing like generating output in a different format or comparing results.

load_run

Type: string Default: ""

Load a saved run. See save_run.

compare_runs

Type: array of string Default: []

Load these saved runs and compare the results. Note that currently only two runs can be compared!

No Additional Items

Each item of this array must be:

Type: string

warn_at

Type: enum (of string) Default: "post"

When to output warnings. Values: 'post' (default): after solving; 'never': no warnings; 'early': for debugging - outputs warnings already while solving (may lead to spurious warnings/asserts that would disappear after narrowing).

Must be one of:

  • "post"
  • "never"
  • "early"

gobview

Type: boolean Default: false

Include additional information for GobView (e.g., the Goblint warning messages) in the directory specified by 'save_run'.

jobs

Type: integer Default: 1

Maximum number of parallel jobs. If 0, then number of cores is used. Currently used for preprocessing and g2html.

goblint-dir

Type: string Default: ".goblint"

Directory used for intermediate data.

Preprocessing

Type: object

Preprocessing options

No Additional Properties

pre.enabled

Type: boolean Default: true

Run the C preprocessor.

pre.keep

Type: boolean Default: false

Keep the intermediate output of running the C preprocessor.

pre.exist

Type: boolean Default: false

Use existing preprocessed files.

pre.includes

Type: array of string Default: []

List of directories to include.

No Additional Items

Each item of this array must be:

Type: string

pre.kernel_includes

Type: array of string Default: []

List of kernel directories to include.

No Additional Items

Each item of this array must be:

pre.custom_includes

Type: array of string Default: []

List of custom directories to include.

No Additional Items

Each item of this array must be:

pre.kernel-root

Type: string Default: ""

Root directory for Linux kernel (linux-headers)

pre.cppflags

Type: array of string Default: []

Pre-processing parameters.

No Additional Items

Each item of this array must be:

Type: string

pre.compdb

Type: object
No Additional Properties

pre.compdb.original-path

Type: string Default: ""

Original absolute path of Compilation Database. Used to reroot all absolute paths in there if moved, e.g. in container mounts.

pre.compdb.split

Type: boolean Default: false

Split Compilation Database entries containing multiple .c files.

pre.transform-paths

Type: boolean Default: true

Normalize and relativize paths in parsed CIL locations. Can cause issues locating YAML witness invariants due to differing paths.

cil

Type: object

CIL configuration

No Additional Properties

cil.merge

Type: object
No Additional Properties

cil.merge.inlines

Type: boolean Default: true

Merge inline functions (by their body printout).

cil.cstd

Type: enum (of string) Default: "c99"

Specify the c standard used for parsing.

Must be one of:

  • "c90"
  • "c99"
  • "c11"

cil.gnu89inline

Type: boolean Default: false

Indicates whether gnu89 semantic should be used for inline functions.

cil.addNestedScopeAttr

Type: boolean Default: false

Indicates whether variables that CIL pulls out of their scope should be marked.

Server

Type: object

Server mode

No Additional Properties

server.enabled

Type: boolean Default: false

Enable server mode

server.mode

Type: enum (of string) Default: "stdio"

Server transport mode

Must be one of:

  • "stdio"
  • "unix"

server.unix-socket

Type: string Default: "goblint.sock"

The path to the UNIX socket

server.reparse

Type: boolean Default: false

Reparse source files before each analysis run

Analyses

Type: object

Options for analyses

No Additional Properties

ana.activated

Type: array of string Default: ["expRelation", "base", "threadid", "threadflag", "threadreturn", "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp", "assert"]

Lists of activated analyses.

No Additional Items

Each item of this array must be:

Type: string

ana.path_sens

Type: array of string Default: ["mutex", "malloc_null", "uninit", "expsplit", "activeSetjmp", "memLeak"]

List of path-sensitive analyses

No Additional Items

Each item of this array must be:

Type: string

ana.ctx_insens

Type: array of string Default: ["stack_loc", "stack_trace_set"]

List of context-insensitive analyses. This setting is ignored if ana.ctx_sens contains elements.

No Additional Items

Each item of this array must be:

Type: string

ana.ctx_sens

Type: array of string Default: []

List of context-sensitive analyses. In case this list is empty, ana.ctx_insens will be used to determine the set of context-insensitive analyses.

No Additional Items

Each item of this array must be:

Type: string

ana.setjmp

Type: object

Setjmp/Longjmp analysis

No Additional Properties

ana.setjmp.split

Type: enum (of string) Default: "precise"

Split returns of setjmp

Must be one of:

  • "none"
  • "coarse"
  • "precise"

ana.int

Type: object
No Additional Properties

ana.int.def_exc

Type: boolean Default: true

Use IntDomain.DefExc: definite value/exclusion set.

ana.int.interval

Type: boolean Default: false

Use IntDomain.Interval32: (Z.t * Z.t) option.

ana.int.interval_set

Type: boolean Default: false

Use IntDomain.IntervalSet: (Z.t * Z.t) list.

ana.int.enums

Type: boolean Default: false

Use IntDomain.Enums: Inclusion/Exclusion sets. Go to top on arithmetic operations (except for some easy cases, e.g. multiplication with 0). Joins on widen, i.e. precise integers as long as not derived from arithmetic expressions.

ana.int.congruence

Type: boolean Default: false

Use IntDomain.Congruence: (c, m) option, meaning congruent to c modulo m

ana.int.refinement

Type: enum (of string) Default: "never"

Use mutual refinement of integer domains. Either 'never', 'once' or 'fixpoint'. Counterintuitively, may reduce precision unless ana.int.intervalnarrowby_meet is also enabled.

Must be one of:

  • "never"
  • "once"
  • "fixpoint"

ana.int.def_exc_widen_by_join

Type: boolean Default: false

Perform def_exc widening by joins. Gives threshold-widening like behavior, with thresholds given by the ranges of different integer types.

ana.int.interval_narrow_by_meet

Type: boolean Default: false

Perform interval narrowing by meets. Avoids precision loss if intervals are refined by def_exc ranges, which are more precise than type range.

ana.int.interval_threshold_widening

Type: boolean Default: false

Use constants appearing in program as threshold for widening

ana.int.interval_threshold_widening_constants

Type: enum (of string) Default: "all"

Which constants in the program should be considered as threshold constants (all/comparisons)

Must be one of:

  • "all"
  • "comparisons"

ana.float

Type: object
No Additional Properties

ana.float.interval

Type: boolean Default: false

Use FloatDomain: (float * float) option.

ana.float.evaluate_math_functions

Type: boolean Default: false

Allow a more precise evaluation of some functions from math.h. Evaluation of functions may differ depending on the implementation of math.h. Caution: For some implementations of functions it is not guaranteed that they behave monotonic where they mathematically should, thus possibly leading to unsoundness.

ana.pml

Type: object
No Additional Properties

ana.pml.debug

Type: boolean Default: true

Insert extra assertions into Promela code for debugging.

ana.opt

Type: object
No Additional Properties

ana.opt.hashcons

Type: boolean Default: true

Should we try to save memory and speed up equality by hashconsing?

ana.opt.equal

Type: boolean Default: true

First try physical equality (==) before {D,G,C}.equal (only done if hashcons is disabled since it basically does the same via its tags).

ana.autotune

Type: object
No Additional Properties

ana.autotune.enabled

Type: boolean Default: false

Try to intelligently select analyses based on analysed file

ana.autotune.activated

Type: array of enum (of string) Default: ["congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification", "termination", "tmpSpecialAnalysis"]

Lists of activated tuning options.

No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "congruence"
  • "singleThreaded"
  • "specification"
  • "mallocWrappers"
  • "noRecursiveIntervals"
  • "enums"
  • "loopUnrollHeuristic"
  • "forceLoopUnrollForFewLoops"
  • "arrayDomain"
  • "octagon"
  • "wideningThresholds"
  • "memsafetySpecification"
  • "termination"
  • "tmpSpecialAnalysis"

ana.sv-comp

Type: object
No Additional Properties

ana.sv-comp.enabled

Type: boolean Default: false

SV-COMP mode

ana.sv-comp.functions

Type: boolean Default: false

Handle SV-COMP __VERIFIER* functions

ana.specification

Type: string Default: ""

SV-COMP specification (path or string)

ana.wp

Type: boolean Default: false

Weakest precondition feasibility analysis for SV-COMP violations

ana.arrayoob

Type: boolean Default: false

Array out of bounds check

ana.base

Type: object
No Additional Properties

ana.base.context

Type: object
No Additional Properties

ana.base.context.non-ptr

Type: boolean Default: true

Non-address values in function contexts.

ana.base.context.int

Type: boolean Default: true

Integer values in function contexts.

ana.base.context.interval

Type: boolean Default: true

Integer values of the Interval domain in function contexts.

ana.base.context.interval_set

Type: boolean Default: true

Integer values of the IntervalSet domain in function contexts.

ana.base.strings

Type: object
No Additional Properties

ana.base.strings.domain

Type: enum (of string) Default: "flat"

Domain for string literals.

Must be one of:

  • "unit"
  • "flat"
  • "disjoint"

ana.base.partition-arrays

Type: object
No Additional Properties

ana.base.partition-arrays.keep-expr

Type: enum (of string) Default: "first"

When using the partitioning which expression should be used for partitioning ('first', 'last')

Must be one of:

  • "first"
  • "last"

ana.base.partition-arrays.partition-by-const-on-return

Type: boolean Default: false

When using the partitioning should arrays be considered partitioned according to a constant if a var in the expression used for partitioning goes out of scope?

ana.base.partition-arrays.smart-join

Type: boolean Default: false

When using the partitioning should the join of two arrays partitioned according to different expressions be partitioned as well if possible? If keep-expr is 'last' this behavior is enabled regardless of the flag value. Caution: Not always advantageous.

ana.base.arrays

Type: object
No Additional Properties

ana.base.arrays.domain

Type: enum (of string) Default: "trivial"

The domain that should be used for arrays. When employing the partition array domain, make sure to enable the expRelation analysis as well. When employing the unrolling array domain, make sure to set the ana.base.arrays.unrolling-factor >0.

Must be one of:

  • "trivial"
  • "partitioned"
  • "unroll"

ana.base.arrays.unrolling-factor

Type: integer Default: 0

Indicates how many values will the unrolled part of the unrolled array domain contain.

ana.base.arrays.nullbytes

Type: boolean Default: false

Whether the Null Byte array domain should be activated.

ana.base.structs

Type: object
No Additional Properties

ana.base.structs.domain

Type: enum (of string) Default: "simple"

The domain that should be used for structs. simple/sets/keyed/combined-all/combined-sk

Must be one of:

  • "simple"
  • "sets"
  • "keyed"
  • "combined-all"
  • "combined-sk"

ana.base.structs.key

Type: object
No Additional Properties

ana.base.structs.key.forward

Type: boolean Default: true

Whether the struct key should be picked going from first field to last.

ana.base.structs.key.avoid-ints

Type: boolean Default: true

Whether integers should be avoided for key.

ana.base.structs.key.prefer-ptrs

Type: boolean Default: true

Whether pointers should be preferred for key.

ana.base.privatization

Type: enum (of string) Default: "protection-read"

Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid

Must be one of:

  • "none"
  • "mutex-oplus"
  • "mutex-meet"
  • "protection"
  • "protection-tid"
  • "protection-atomic"
  • "protection-read"
  • "protection-read-tid"
  • "protection-read-atomic"
  • "mine"
  • "mine-nothread"
  • "mine-W"
  • "mine-W-noinit"
  • "lock"
  • "lock-tid"
  • "write"
  • "write-tid"
  • "write+lock"
  • "write+lock-tid"
  • "mutex-meet-tid"

ana.base.priv

Type: object
No Additional Properties

ana.base.priv.not-started

Type: boolean Default: true

Exclude writes from threads that may not be started yet

ana.base.priv.must-joined

Type: boolean Default: true

Exclude writes from threads that must have been joined

ana.base.invariant

Type: object
No Additional Properties

ana.base.invariant.enabled

Type: boolean Default: true

Generate base analysis invariants

ana.base.invariant.blobs

Type: boolean Default: false

Whether to dump assertions about all blobs. Enabling this option may lead to unsound asserts.

ana.base.invariant.unassume

Type: enum (of string) Default: "once"

How many times to unassume an invariant: once or until fixpoint (at least twice as expensive).

Must be one of:

  • "once"
  • "fixpoint"

ana.base.eval

Type: object
No Additional Properties

ana.base.eval.deep-query

Type: boolean Default: true

Perform EvalInt queries on all subexpressions, not just the outermost expression.

ana.malloc

Type: object
No Additional Properties

ana.malloc.wrappers

Type: array of string Default: ["kmalloc", "__kmalloc", "usb_alloc_urb", "__builtin_alloca", "kzalloc"]

Loads a list of known malloc wrapper functions.

No Additional Items

Each item of this array must be:

Type: string

ana.malloc.unique_address_count

Type: integer Default: 0

Number of unique memory addresses allocated for each malloc node.

ana.apron

Type: object
No Additional Properties

ana.apron.strengthening

Type: boolean Default: false

Apply strengthening in join for extra precision with heterogeneous environments. Expensive!

ana.apron.domain

Type: enum (of string) Default: "octagon"

Which domain should be used for the Apron analysis. Can be 'octagon', 'interval' or 'polyhedra'

Must be one of:

  • "octagon"
  • "interval"
  • "polyhedra"
  • "affeq"

ana.apron.threshold_widening

Type: boolean Default: false

Use constants appearing in program as threshold for widening

ana.apron.threshold_widening_constants

Type: enum (of string) Default: "all"

Which constants in the programm should be considered as threshold constants

Must be one of:

  • "all"
  • "comparisons"

ana.apron.invariant

Type: object
No Additional Properties

ana.apron.invariant.diff-box

Type: boolean Default: false

Only generate truly relational invariants by subtracting non-relational box invariants

ana.relation

Type: object
No Additional Properties

ana.relation.context

Type: boolean Default: true

Entire relation in function contexts.

ana.relation.privatization

Type: enum (of string) Default: "mutex-meet"

Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power

Must be one of:

  • "top"
  • "protection"
  • "protection-path"
  • "mutex-meet"
  • "mutex-meet-atomic"
  • "mutex-meet-tid"
  • "mutex-meet-tid-atomic"
  • "mutex-meet-tid-cluster12"
  • "mutex-meet-tid-cluster2"
  • "mutex-meet-tid-cluster-max"
  • "mutex-meet-tid-cluster-power"

ana.relation.priv

Type: object
No Additional Properties

ana.relation.priv.not-started

Type: boolean Default: true

Exclude writes from threads that may not be started yet

ana.relation.priv.must-joined

Type: boolean Default: true

Exclude writes from threads that must have been joined

ana.relation.invariant

Type: object
No Additional Properties

ana.relation.invariant.one-var

Type: boolean Default: false

Generate invariants with only one variable

ana.relation.invariant.local

Type: boolean Default: true

Keep local variables in invariants

ana.relation.invariant.global

Type: boolean Default: true

Keep global variables in invariants

ana.context

Type: object
No Additional Properties

ana.context.widen

Type: boolean Default: false

Do widening on contexts. Keeps a map of function to call state; enter will then return the widened local state for recursive calls.

ana.context.gas_value

Type: integer Default: -1

Denotes the gas value x for the ContextGasLifter. Negative values deactivate the context gas, zero yields a context-insensitve analysis. If enabled, the first x recursive calls of the call stack are analyzed context-sensitively. Any calls deeper in the call stack are analyzed with the same (empty) context.

ana.context.callString_length

Type: integer Default: 2

Length of the call string that should be used as context for the callstring and/or callsite analyses. In case the value is zero, the analysis is context-insensitive. For a negative value, an infinite call string is used! For this option to have an effect, one of the analyses in callstring.ml must be activated.

ana.thread

Type: object
No Additional Properties

ana.thread.domain

Type: enum (of string) Default: "history"

Which domain should be used for the thread ids. Can be 'history' or 'plain'

Must be one of:

  • "history"
  • "plain"

ana.thread.include-node

Type: boolean Default: true

Whether the node at which a thread is created is part of its threadid

ana.thread.wrappers

Type: array of string Default: []

Loads a list of known thread spawn (pthread_create) wrapper functions.

No Additional Items

Each item of this array must be:

Type: string

ana.thread.unique_thread_id_count

Type: integer Default: 0

Number of unique thread IDs allocated for each pthread_create node.

ana.thread.context

Type: object
No Additional Properties

ana.thread.context.create-edges

Type: boolean Default: true

threadID analysis: Encountered create edges in context.

ana.race

Type: object
No Additional Properties

ana.race.free

Type: boolean Default: true

Consider memory free as racing write.

ana.race.call

Type: boolean Default: true

Report races for thread-unsafe function calls.

ana.race.direct-arithmetic

Type: boolean Default: false

Collect and distribute direct (i.e. not in a field) accesses to arithmetic types.

ana.race.volatile

Type: boolean Default: true

Report races for volatile variables.

ana.dead-code

Type: object
No Additional Properties

ana.dead-code.lines

Type: boolean Default: true

Print information about lines of dead code.

ana.dead-code.branches

Type: boolean Default: true

Print information about dead branches.

ana.dead-code.functions

Type: boolean Default: true

Print information about dead (uncalled) functions.

ana.extract-pthread

Type: object
No Additional Properties

ana.extract-pthread.assume_success

Type: boolean Default: true

Assume that all POSIX pthread functions succeed.

ana.extract-pthread.ignore_assign

Type: boolean Default: true

Ignores any assigns in POSIX programs.

ana.widen

Type: object
No Additional Properties

ana.widen.tokens

Type: boolean Default: false

Delay widenings using widening tokens.

ana.unassume

Type: object
No Additional Properties

ana.unassume.precheck

Type: boolean Default: false

Check if invariant contradicts reached state before unassuming.

Incremental

Type: object

Incremental analysis options

No Additional Properties

incremental.load

Type: boolean Default: false

Load incremental analysis results, in case any exist.

incremental.load-dir

Type: string Default: "incremental_data"

Location where to load incremental analysis results from.

incremental.only-rename

Type: boolean Default: false

Only reset IDs of unchanged objects in the AST. Do not reuse solver results. This option is mainly useful for benchmarking purposes.

incremental.save

Type: boolean Default: false

Store incremental analysis results.

incremental.save-dir

Type: string Default: "incremental_data"

Location where to save incremental analysis results to.

incremental.stable

Type: boolean Default: true

Reuse the stable set and selectively destabilize it (recommended).

incremental.wpoint

Type: boolean Default: false

Reuse the wpoint set (not recommended). Reusing the wpoint will combine existing results at previous widening points.

incremental.reluctant

Type: object
No Additional Properties

incremental.reluctant.enabled

Type: boolean Default: false

Destabilize nodes in changed functions reluctantly

incremental.compare

Type: enum (of string) Default: "ast"

Which comparison should be used for functions? 'ast'/'cfg' (cfg comparison also differentiates which nodes of a function have changed)

Must be one of:

  • "ast"
  • "cfg"

incremental.detect-renames

Type: boolean Default: true

If Goblint should try to detect renamed local variables, function parameters, functions and global variables

incremental.force-reanalyze

Type: object
No Additional Properties

incremental.force-reanalyze.funs

Type: array of string Default: []

List of functions that are to be re-analayzed from scratch

No Additional Items

Each item of this array must be:

incremental.restart

Type: object
No Additional Properties

incremental.restart.sided

Type: object
No Additional Properties

incremental.restart.sided.enabled

Type: boolean Default: false

Restart affected side-effected variables (transitively) to bot.

incremental.restart.sided.vars

Type: enum (of string) Default: "all"

Side-effected variables to restart. Globals are non-function entry nodes. Write-only is a subset of globals.

Must be one of:

  • "all"
  • "global"
  • "write-only"

incremental.restart.sided.fuel

Type: integer Default: -1

Initial fuel for bounding transitive restarting, which uses one fuel each time when following side_fuel to restart. Zero fuel never restarts. Negative fuel doesn't bound (infinite fuel).

incremental.restart.sided.fuel-only-global

Type: boolean Default: false

Decrease fuel only when going to constraint system globals (not function entry nodes).

incremental.restart.list

Type: array of string Default: []

List of globals variables and function definitions for which the analysis is to be restarted.

No Additional Items

Each item of this array must be:

Type: string

incremental.restart.write-only

Type: boolean Default: true

Restart write-only variables to bot during postprocessing.

incremental.postsolver

Type: object
No Additional Properties

incremental.postsolver.enabled

Type: boolean Default: true

Use incremental postsolver

incremental.postsolver.superstable-reached

Type: boolean Default: false

Consider superstable set reached, may be faster but can lead to spurious warnings

Library functions

Type: object

Options for library functions

No Additional Properties

lib.activated

Type: array of enum (of string) Default: ["c", "posix", "pthread", "gcc", "glibc", "linux-userspace", "goblint", "ncurses", "legacy"]

List of activated libraries.

No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "c"
  • "posix"
  • "pthread"
  • "gcc"
  • "glibc"
  • "linux-userspace"
  • "linux-kernel"
  • "goblint"
  • "sv-comp"
  • "klever"
  • "ncurses"
  • "zstd"
  • "pcre"
  • "zlib"
  • "liblzma"
  • "legacy"

Semantics

Type: object

Options for semantics

No Additional Properties

sem.unknown_function

Type: object
No Additional Properties

sem.unknown_function.spawn

Type: boolean Default: true

Unknown function call spawns reachable functions

sem.unknown_function.call

Type: boolean Default: true

Unknown function call calls reachable functions

sem.unknown_function.invalidate

Type: object
No Additional Properties

sem.unknown_function.invalidate.globals

Type: boolean Default: true

Unknown function call invalidates all globals

sem.unknown_function.invalidate.args

Type: boolean Default: true

Unknown function call invalidates arguments passed to it

sem.unknown_function.read

Type: object
No Additional Properties

sem.unknown_function.read.args

Type: boolean Default: true

Unknown function call reads arguments passed to it

sem.builtin_unreachable

Type: object
No Additional Properties

sem.builtin_unreachable.dead_code

Type: boolean Default: false

_builtinunreachable is assumed to be dead code

sem.noreturn

Type: object

Handling of C11 _Noreturn function specifier.

No Additional Properties

sem.noreturn.dead_code

Type: boolean Default: false

For the purposes of detecting dead code, assume that functions marked noreturn don't return.

sem.int

Type: object
No Additional Properties

sem.int.signed_overflow

Type: enum (of string) Default: "assume_top"

How to handle overflows of signed types. Values: 'assumetop' (default): Assume signed overflow results in a top value; 'assumenone': Assume program is free of signed overflows; 'assume_wraparound': Assume signed types wrap-around and two's complement representation of signed integers

Must be one of:

  • "assume_top"
  • "assume_none"
  • "assume_wraparound"

sem.null-pointer

Type: object
No Additional Properties

sem.null-pointer.dereference

Type: enum (of string) Default: "assume_none"

NULL pointer dereference handling. assumetop: assume it results in a top value, assumenone: assume it doesn't happen

Must be one of:

  • "assume_top"
  • "assume_none"

sem.malloc

Type: object
No Additional Properties

sem.malloc.fail

Type: boolean Default: false

Consider the case where malloc or calloc fails.

sem.lock

Type: object
No Additional Properties

sem.lock.fail

Type: boolean Default: false

Takes the possible failing of locking operations into account.

sem.assert

Type: object
No Additional Properties

sem.assert.refine

Type: boolean Default: true

Standard assert refines state

Transformations

Type: object

Options for transformations

No Additional Properties

trans.activated

Type: array of enum (of string) Default: []

Lists of activated transformations. Transformations happen after analyses.

No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "partial"
  • "expeval"
  • "assert"
  • "remove_dead_code"

trans.expeval

Type: object
No Additional Properties

trans.expeval.query_file_name

Type: string Default: ""

Path to the JSON file containing an expression evaluation query.

trans.output

Type: string Default: "transformed.c"

Output filename for transformations that output a transformed file.

Annotation

Type: object

Options for annotations

No Additional Properties

annotation.int

Type: object
No Additional Properties

annotation.int.enabled

Type: boolean Default: false

Enable manual annotation of functions with desired precision, i.e., the activated IntDomains.

annotation.int.privglobs

Type: boolean Default: true

Enables handling of privatized globals, by setting the precision to the heighest value, when annotation.int.enabled is true.

annotation.float

Type: object
No Additional Properties

annotation.float.enabled

Type: boolean Default: false

Enable manual annotation of functions with desired precision, i.e., the activated FloatDomains.

annotation.goblint_context

Type: object

Each additional property must conform to the following schema

Type: array of enum (of string) Default: []
No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "base.no-non-ptr"
  • "base.non-ptr"
  • "base.no-int"
  • "base.int"
  • "base.no-interval"
  • "base.no-interval_set"
  • "base.interval"
  • "base.interval_set"
  • "relation.no-context"
  • "relation.context"
  • "no-widen"
  • "widen"

annotation.goblint_precision

Type: object

Each additional property must conform to the following schema

Type: array of enum (of string) Default: []
No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "no-def_exc"
  • "def_exc"
  • "no-interval"
  • "interval"
  • "no-enums"
  • "enums"
  • "no-congruence"
  • "congruence"

annotation.goblint_array_domain

Type: boolean Default: false

Enable manual annotation of arrays with desired domain

annotation.goblint_relation_track

Type: boolean Default: false

Let relation track variables only if they have the attribute goblintrelationtrack

Experimental

Type: object

Experimental features

No Additional Properties

exp.priv-prec-dump

Type: string Default: ""

File to dump privatization precision data to.

exp.priv-distr-init

Type: boolean Default: false

Distribute global initializations to all global invariants for more consistent widening dynamics.

exp.relation

Type: object
No Additional Properties

exp.relation.prec-dump

Type: string Default: ""

File to dump relation precision data to.

exp.cfgdot

Type: boolean Default: false

Output CFG to dot files

exp.mincfg

Type: boolean Default: false

Try to minimize the number of CFG nodes.

exp.earlyglobs

Type: boolean Default: false

Side-effecting of globals right after initialization.

exp.region-offsets

Type: boolean Default: false

Considers offsets for region accesses.

exp.unique

Type: array of string Default: []

For types that have only one value.

No Additional Items

Each item of this array must be:

Type: string

exp.forward

Type: boolean Default: false

Use implicit forward propagation instead of the demand driven approach.

exp.volatiles_are_top

Type: boolean Default: true

volatile and extern keywords set variables permanently to top

exp.single-threaded

Type: boolean Default: false

Ensures analyses that no threads are created.

exp.globs_are_top

Type: boolean Default: false

Set globals permanently to top.

exp.exclude_from_earlyglobs

Type: array of string Default: []

Global variables that should be handled flow-sensitively when using earlyglobs.

No Additional Items

Each item of this array must be:

exp.exclude_from_invalidation

Type: array of string Default: []

Global variables that should not be invalidated. This assures the analysis that such globals are only modified through known code

No Additional Items

Each item of this array must be:

exp.g2html_path

Type: string Default: ""

Location of the g2html.jar file. If empty, then goblint executable directory is used.

exp.extraspecials

Type: array of string Default: []

List of functions that must be analyzed as unknown extern functions

No Additional Items

Each item of this array must be:

exp.no-narrow

Type: boolean Default: false

Overwrite narrow a b = a

exp.basic-blocks

Type: boolean Default: false

Only keep values for basic blocks instead of for every node. Should take longer but need less space.

exp.fast_global_inits

Type: boolean Default: true

Only generate one 'a[any_index] = x' for all assignments a[...] = x for a global array a[n].

exp.architecture

Type: enum (of string) Default: "64bit"

Architecture for analysis, currently for witness

Must be one of:

  • "64bit"
  • "32bit"

exp.gcc_path

Type: string Default: "/usr/bin/gcc"

Location of gcc. Used to combine source files with cilly. Change to gcc-9 or another version on OS X (with gcc being clang by default cilly will fail otherwise).

exp.cpp-path

Type: string Default: ""

Path to C preprocessor (cpp) to use. If empty, then automatically searched.

exp.unrolling-factor

Type: integer Default: 0

Sets the unrolling factor for the loopUnrollingVisitor.

exp.hide-std-globals

Type: boolean Default: true

Hide standard extern globals (e.g. stdout) from cluttering local states.

exp.arg

Type: boolean Default: false

Construct abstract reachability graph (ARG).

exp.argdot

Type: boolean Default: false

Output ARG as dot file.

Debugging

Type: object

Debugging options

No Additional Properties

dbg.level

Type: enum (of string) Default: "info"

Logging level.

Must be one of:

  • "debug"
  • "info"
  • "warning"
  • "error"
  • "result"

dbg.timing

Type: object
No Additional Properties

dbg.timing.enabled

Type: boolean Default: false

Collect and output timing information.

dbg.timing.tef

Type: string Default: ""

Filename for Trace Event Format (TEF) output. Disabled if empty.

dbg.trace

Type: object
No Additional Properties

dbg.trace.context

Type: boolean Default: false

Also print the context of solver variables.

dbg.dump

Type: string Default: ""

Dumps the results to the given path

dbg.cilout

Type: string Default: ""

Where to dump cil output

dbg.justcil-printer

Type: enum (of string) Default: "default"

Printer to use for justcil: default, or clean (excludes line directives and builtin declarations).

Must be one of:

  • "default"
  • "clean"

dbg.timeout

Type: string Default: "0"

Stop solver after this time. 0 means no timeout. Supports optional units h, m, s. E.g. 1m6s = 01m06s = 66; 6h = 66060.

dbg.solver-stats-interval

Type: integer Default: 10

Interval in seconds to print statistics while solving. Set to 0 to deactivate.

dbg.solver-signal

Type: string Default: "sigusr1"

Signal to print statistics while solving. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+), sigusr1, sigusr2, sigalrm, sigprof etc. (see signalofstring in gobSys.ml).

dbg.backtrace-signal

Type: string Default: "sigusr2"

Signal to print a raw backtrace on stderr. Possible values: sigint (Ctrl+C), sigtstp (Ctrl+Z), sigquit (Ctrl+), sigusr1, sigusr2, sigalrm, sigprof etc. (see signalofstring in gobSys.ml).

dbg.solver-progress

Type: boolean Default: false

Used for debugging. Prints out a symbol on solving a rhs.

dbg.print_wpoints

Type: boolean Default: false

Print the widening points after solving (does not include the removed wpoints during solving by the slr solvers). Currently only implemented in: slr*, td3.

dbg.slice

Type: object
No Additional Properties

dbg.slice.on

Type: boolean Default: false

Turn slicer on or off.

dbg.slice.n

Type: integer Default: 10

How deep function stack do we analyze.

dbg.limit

Type: object
No Additional Properties

dbg.limit.widen

Type: integer Default: 0

Limit for number of widenings per node (0 = no limit).

dbg.warn_with_context

Type: boolean Default: false

Keep warnings for different contexts apart (currently only done for asserts).

dbg.regression

Type: boolean Default: false

Only output warnings for assertions that have an unexpected result (no comment, comment FAIL, comment UNKNOWN)

dbg.test

Type: object
No Additional Properties

dbg.test.domain

Type: boolean Default: false

Test domain properties

dbg.cilcfgdot

Type: boolean Default: false

Output dot files for CIL CFGs.

dbg.cfg

Type: object
No Additional Properties

dbg.cfg.loop-clusters

Type: boolean Default: false

Add loop SCC clusters to CFG .dot output.

dbg.cfg.loop-unrolling

Type: boolean Default: false

Add dotted loop unrolling copy-of edges to CFG .dot output.

dbg.compare_runs

Type: object
No Additional Properties

dbg.compare_runs.globsys

Type: boolean Default: false

Compare GlobConstrSys in compare_runs

dbg.compare_runs.eqsys

Type: boolean Default: true

Compare EqConstrSys in compare_runs

dbg.compare_runs.global

Type: boolean Default: false

Compare globals in compare_runs

dbg.compare_runs.node

Type: boolean Default: false

Compare nodes (with joined contexts) in compare_runs

dbg.compare_runs.diff

Type: boolean Default: false

Print differences

dbg.print_tids

Type: boolean Default: false

Should the analysis print information on the encountered TIDs

dbg.print_protection

Type: boolean Default: false

Should the analysis print information on which globals are protected by which mutex?

dbg.run_cil_check

Type: boolean Default: false

Should the analysis call Check.checkFile after creating the CFG (helpful to verify that transformations respect CIL's invariants.

dbg.full-output

Type: boolean Default: false

Output abstract values, etc. with full internal details, without readability-oriented simplifications.

Warnings

Type: object

Filtering of warnings

No Additional Properties

warn.assert

Type: boolean Default: true

Assert messages

warn.behavior

Type: boolean Default: true

undefined behavior warnings

warn.call

Type: boolean Default: true

function call warnings

warn.integer

Type: boolean Default: true

integer (Overflow, Divbyzero) warnings

warn.float

Type: boolean Default: true

float warnings

warn.cast

Type: boolean Default: true

Cast (Type_mismatch(bug) warnings

warn.race

Type: boolean Default: true

Race warnings

warn.deadlock

Type: boolean Default: true

Deadlock warnings

warn.deadcode

Type: boolean Default: true

Dead code warnings

warn.analyzer

Type: boolean Default: true

Analyzer messages

warn.unsound

Type: boolean Default: true

Unsoundness messages

warn.imprecise

Type: boolean Default: true

Imprecision messages

warn.witness

Type: boolean Default: true

Witness messages

warn.program

Type: boolean Default: true

Program messages

warn.termination

Type: boolean Default: true

Non-Termination warning

warn.unknown

Type: boolean Default: true

Unknown (of string) warnings

warn.error

Type: boolean Default: true

Error severity messages

warn.warning

Type: boolean Default: true

Warning severity messages

warn.info

Type: boolean Default: true

Info severity messages

warn.debug

Type: boolean Default: false

Debug severity messages

warn.success

Type: boolean Default: true

Success severity messages

warn.quote-code

Type: boolean Default: false

Quote code in message output.

warn.race-threshold

Type: integer Default: 0

Races with confidence at least threshold are warnings, lower are infos.

warn.deterministic

Type: boolean Default: false

Output messages in deterministic order. Useful for cram testing.

warn.memleak

Type: object
No Additional Properties

warn.memleak.memcleanup

Type: boolean Default: false

Enable memory leak warnings only for violations of the SV-COMP "valid-memcleanup" category

warn.memleak.memtrack

Type: boolean Default: false

Enable memory leak warnings only for violations of the SV-COMP "valid-memtrack" category

solvers

Type: object
No Additional Properties

solvers.td3

Type: object
No Additional Properties

solvers.td3.term

Type: boolean Default: true

Should the td3 solver use the phased/terminating strategy?

solvers.td3.side_widen

Type: enum (of string) Default: "sides"

When to widen in side. never: never widen, always: always widen, sides: widen if there are multiple side-effects from the same var resulting in a new value, cycle: widen if a called or a start var get destabilized, unstablecalled: widen if any called var gets destabilized, unstableself: widen if side-effected var gets destabilized, sides-pp: widen if there are multiple side-effects from the same program point resulting in a new value, sides-local: Widen with contributions from variables from which multiple side-effects leading to a new value originate.

Must be one of:

  • "never"
  • "always"
  • "sides"
  • "cycle"
  • "unstable_called"
  • "unstable_self"
  • "sides-pp"
  • "sides-local"

solvers.td3.space

Type: boolean Default: false

Should the td3 solver only keep values at widening points?

solvers.td3.space_cache

Type: boolean Default: true

Should the td3-space solver cache values?

solvers.td3.space_restore

Type: boolean Default: true

Should the td3-space solver restore values for non-widening-points? Not needed for generating warnings, but needed for inspecting output!

solvers.td3.narrow-reuse

Type: boolean Default: true

Reuse value when switching from widening to narrowing phase. Avoids one unnecessary re-evaluation.

solvers.td3.remove-wpoint

Type: boolean Default: true

Remove widening points after narrowing phase. Enables a form of local restarting which increases precision of nested loops.

solvers.td3.skip-unchanged-rhs

Type: boolean Default: false

Skip evaluation of RHS if all dependencies are unchanged - INCOMPATIBLE WITH RESTARTING

solvers.td3.restart

Type: object
No Additional Properties

solvers.td3.restart.wpoint

Type: object
No Additional Properties

solvers.td3.restart.wpoint.enabled

Type: boolean Default: false

Restart wpoint to bot when (re-)detected. Allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted).

solvers.td3.restart.wpoint.once

Type: boolean Default: false

Restart wpoint only on first detection. Useful for incremental loading.

solvers.td3.verify

Type: boolean Default: false

Check TD3 data structure invariants

solvers.slr4

Type: object
No Additional Properties

solvers.slr4.restart_count

Type: integer Default: 1

How many times SLR4 is allowed to switch from restarting iteration to increasing iteration.

witness

Type: object
No Additional Properties

witness.graphml

Type: object
No Additional Properties

witness.graphml.enabled

Type: boolean Default: false

Output GraphML witness

witness.graphml.path

Type: string Default: "witness.graphml"

GraphML witness output path

witness.graphml.id

Type: enum (of string) Default: "node"

Which witness node IDs to use? node/enumerate

Must be one of:

  • "node"
  • "enumerate"

witness.graphml.minimize

Type: boolean Default: false

Try to minimize the witness

witness.graphml.uncil

Type: boolean Default: false

Try to undo CIL control flow transformations in witness

witness.graphml.stack

Type: boolean Default: true

Construct stacktrace-based witness nodes

witness.graphml.unknown

Type: boolean Default: true

Output witness for unknown result

witness.invariant

Type: object
No Additional Properties

witness.invariant.loop-head

Type: boolean Default: true

Emit invariants at loop heads

witness.invariant.after-lock

Type: boolean Default: true

Emit invariants after mutex locking

witness.invariant.other

Type: boolean Default: true

Emit invariants at all other locations

witness.invariant.split-conjunction

Type: boolean Default: true

Split conjunctive invariant to multiple invariants

witness.invariant.accessed

Type: boolean Default: false

Only emit invariants for locally accessed variables

witness.invariant.full

Type: boolean Default: true

Whether to dump assertions about all local variables or limitting it to modified ones where possible.

witness.invariant.exact

Type: boolean Default: true

Emit exact invariants. They are useless for unassuming.

witness.invariant.inexact-type-bounds

Type: boolean Default: false

Emit inexact invariants matching type bounds.

witness.invariant.exclude-vars

Type: array of string Default: ["tmp\\(___[0-9]+\\)?", "cond", "RETURN"]

OCaml Str regexes for variables to exclude from invariants.

No Additional Items

Each item of this array must be:

witness.invariant.all-locals

Type: boolean Default: true

Emit invariants for local variables under the assumption they are always in scope within their function.

witness.invariant.goblint

Type: boolean Default: false

Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.

witness.invariant.typedefs

Type: boolean Default: true

Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.

witness.yaml

Type: object
No Additional Properties

witness.yaml.enabled

Type: boolean Default: false

Output YAML witness

witness.yaml.format-version

Type: enum (of string) Default: "0.1"

YAML witness format version

Must be one of:

  • "0.1"
  • "2.0"

witness.yaml.entry-types

Type: array of enum (of string) Default: ["location_invariant", "loop_invariant", "flow_insensitive_invariant", "loop_invariant_certificate", "precondition_loop_invariant_certificate", "invariant_set"]

YAML witness entry types to output/input.

No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "location_invariant"
  • "loop_invariant"
  • "flow_insensitive_invariant"
  • "precondition_loop_invariant"
  • "loop_invariant_certificate"
  • "precondition_loop_invariant_certificate"
  • "invariant_set"

witness.yaml.invariant-types

Type: array of enum (of string) Default: ["location_invariant", "loop_invariant"]

YAML witness invariant types to output/input.

No Additional Items

Each item of this array must be:

Type: enum (of string)

Must be one of:

  • "location_invariant"
  • "loop_invariant"

witness.yaml.path

Type: string Default: "witness.yml"

YAML witness output path

witness.yaml.validate

Type: string Default: ""

YAML witness input path

witness.yaml.strict

Type: boolean Default: false

witness.yaml.unassume

Type: string Default: ""

YAML witness input path

witness.yaml.certificate

Type: string Default: ""

YAML witness certificate output path