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

Split Compilation Database entries containing multiple .c files.

Merge inline functions (by their body printout).

Split returns of setjmp

Use IntDomain.DefExc: definite value/exclusion set.

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

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

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.

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

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

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

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

Use constants appearing in program as threshold for widening

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

Use FloatDomain: (float * float) option.

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.

Insert extra assertions into Promela code for debugging.

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

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

Try to intelligently select analyses based on analysed file

Lists of activated tuning options.

SV-COMP mode

Handle SV-COMP __VERIFIER* functions

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

Loads a list of known malloc wrapper functions.

Number of unique memory addresses allocated for each malloc node.

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

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

Use constants appearing in program as threshold for widening

Which constants in the programm should be considered as threshold constants

Entire relation in function contexts.

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

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

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.

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.

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

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

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

Number of unique thread IDs allocated for each pthread_create node.

Consider memory free as racing write.

Report races for thread-unsafe function calls.

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

Report races for volatile variables.

Print information about lines of dead code.

Print information about dead branches.

Print information about dead (uncalled) functions.

Assume that all POSIX pthread functions succeed.

Ignores any assigns in POSIX programs.

Delay widenings using widening tokens.

Check if invariant contradicts reached state before unassuming.

Destabilize nodes in changed functions reluctantly

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

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

Restart write-only variables to bot during postprocessing.

Use incremental postsolver

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

Unknown function call spawns reachable functions

Unknown function call calls reachable functions

_builtinunreachable is assumed to be dead code

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

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

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

Consider the case where malloc or calloc fails.

Takes the possible failing of locking operations into account.

Standard assert refines state

Path to the JSON file containing an expression evaluation query.

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

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

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

File to dump relation precision data to.

Collect and output timing information.

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

Also print the context of solver variables.

Turn slicer on or off.

How deep function stack do we analyze.

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

Test domain properties

Add loop SCC clusters to CFG .dot output.

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

Compare GlobConstrSys in compare_runs

Compare EqConstrSys in compare_runs

Compare globals in compare_runs

Compare nodes (with joined contexts) in compare_runs

Print differences

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

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

Should the td3 solver use the phased/terminating strategy?

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.

Should the td3 solver only keep values at widening points?

Should the td3-space solver cache values?

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

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