mainfun
Type: array of string Default: ["main"]Sets the name of the main functions.
No Additional ItemsFiles to analyze.
No Additional ItemsFile to print output to.
Just parse and output the CIL.
Only output the CFG in cfg.dot .
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!
Sets the name of the main functions.
No Additional ItemsSets the name of the cleanup functions.
No Additional ItemsSets the name of other functions.
No Additional ItemsPrints access information about all globals, not just races.
For analyzing Linux Device Drivers.
Print out the global invariant.
Result style: none, fast_xml, json, pretty, pretty-deterministic, json-messages, sarif.
Picks the solver.
Picks another solver for comparison.
Analyzes all the functions (not just beginning from main). This requires exp.earlyglobs!
Analyzes all non-static functions.
Colored output (via ANSI escape codes). 'auto': enabled if stdout is a terminal (instead of a pipe); 'always', 'never'.
Run g2html.jar on the generated xml.
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 a saved run. See save_run.
Load these saved runs and compare the results. Note that currently only two runs can be compared!
No Additional ItemsWhen 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).
Include additional information for GobView (e.g., the Goblint warning messages) in the directory specified by 'save_run'.
Maximum number of parallel jobs. If 0, then number of cores is used. Currently used for preprocessing and g2html.
Directory used for intermediate data.
Preprocessing options
No Additional PropertiesRun the C preprocessor.
Keep the intermediate output of running the C preprocessor.
Use existing preprocessed files.
List of directories to include.
No Additional ItemsList of kernel directories to include.
No Additional ItemsList of custom directories to include.
No Additional ItemsRoot directory for Linux kernel (linux-headers)
Pre-processing parameters.
No Additional ItemsOriginal 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.
Normalize and relativize paths in parsed CIL locations. Can cause issues locating YAML witness invariants due to differing paths.
CIL configuration
No Additional PropertiesMerge inline functions (by their body printout).
Specify the c standard used for parsing.
Indicates whether gnu89 semantic should be used for inline functions.
Indicates whether variables that CIL pulls out of their scope should be marked.
Server mode
No Additional PropertiesEnable server mode
Server transport mode
The path to the UNIX socket
Reparse source files before each analysis run
Options for analyses
No Additional PropertiesLists of activated analyses.
No Additional ItemsList of path-sensitive analyses
No Additional ItemsList of context-insensitive analyses. This setting is ignored if ana.ctx_sens
contains elements.
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.
Setjmp/Longjmp analysis
No Additional PropertiesSplit 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.
No Additional ItemsSV-COMP mode
Handle SV-COMP __VERIFIER* functions
SV-COMP specification (path or string)
Weakest precondition feasibility analysis for SV-COMP violations
Array out of bounds check
Non-address values in function contexts.
Integer values in function contexts.
Integer values of the Interval domain in function contexts.
Integer values of the IntervalSet domain in function contexts.
Domain for string literals.
When using the partitioning which expression should be used for partitioning ('first', 'last')
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?
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.
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.
Indicates how many values will the unrolled part of the unrolled array domain contain.
Whether the Null Byte array domain should be activated.
The domain that should be used for structs. simple/sets/keyed/combined-all/combined-sk
Whether the struct key should be picked going from first field to last.
Whether integers should be avoided for key.
Whether pointers should be preferred for key.
Which privatization to use? none/vojdani/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
Exclude writes from threads that may not be started yet
Exclude writes from threads that must have been joined
Generate base analysis invariants
Keep local variables in invariants
Keep global variables in invariants
Whether to dump assertions about all blobs. Enabling this option may lead to unsound asserts.
How many times to unassume an invariant: once or until fixpoint (at least twice as expensive).
How much to simplify int domain invariants. Value "int" only simplifies definite integers. Without int domain refinement "all" might not be maximally precise.
Perform EvalInt queries on all subexpressions, not just the outermost expression.
Loads a list of known malloc wrapper functions.
No Additional ItemsNumber 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
Only generate truly relational invariants by subtracting non-relational box invariants
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
Exclude writes from threads that may not be started yet
Exclude writes from threads that must have been joined
Generate invariants with only one variable
Keep local variables in invariants
Keep global variables in invariants
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-insensitive 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.
Whether the gas should be 'global' (default) or per 'function'
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.
No Additional ItemsNumber of unique thread IDs allocated for each pthread_create node.
threadID analysis: Encountered create edges in context.
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.
Generate var_eq analysis invariants
Incremental analysis options
No Additional PropertiesLoad incremental analysis results, in case any exist.
Location where to load incremental analysis results from.
Only reset IDs of unchanged objects in the AST. Do not reuse solver results. This option is mainly useful for benchmarking purposes.
Store incremental analysis results.
Location where to save incremental analysis results to.
Reuse the stable set and selectively destabilize it (recommended).
Reuse the wpoint set (not recommended). Reusing the wpoint will combine existing results at previous widening points.
Destabilize nodes in changed functions reluctantly
Which comparison should be used for functions? 'ast'/'cfg' (cfg comparison also differentiates which nodes of a function have changed)
If Goblint should try to detect renamed local variables, function parameters, functions and global variables
List of functions that are to be re-analayzed from scratch
No Additional ItemsRestart affected side-effected variables (transitively) to bot.
Side-effected variables to restart. Globals are non-function entry nodes. Write-only is a subset of globals.
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).
Decrease fuel only when going to constraint system globals (not function entry nodes).
List of globals variables and function definitions for which the analysis is to be restarted.
No Additional ItemsRestart write-only variables to bot during postprocessing.
Use incremental postsolver
Consider superstable set reached, may be faster but can lead to spurious warnings
Options for library functions
No Additional PropertiesList of activated libraries.
No Additional ItemsOptions for semantics
No Additional PropertiesUnknown function call spawns reachable functions
Unknown function call calls reachable functions
Unknown function call invalidates all globals
Unknown function call invalidates arguments passed to it
Unknown function call reads arguments passed to it
_builtinunreachable is assumed to be dead code
Handling of C11 _Noreturn function specifier.
No Additional PropertiesFor 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
Ignore atexit callbacks (unsound).
Options for transformations
No Additional PropertiesLists of activated transformations. Transformations happen after analyses.
No Additional ItemsPath to the JSON file containing an expression evaluation query.
Output filename for transformations that output a transformed file.
Function to use for assertions in output.
Wrap assertions in _VERIFIERatomicbegin and _VERIFIERatomicend.
Options for annotations
No Additional PropertiesEnable 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.
Each additional property must conform to the following schema
Type: array of enum (of string) Default: []Each additional property must conform to the following schema
Type: array of enum (of string) Default: []Enable manual annotation of arrays with desired domain
Let relation track variables only if they have the attribute goblintrelationtrack
Experimental features
No Additional PropertiesFile to dump privatization precision data to.
Distribute global initializations to all global invariants for more consistent widening dynamics.
File to dump relation precision data to.
Output CFG to dot files
Try to minimize the number of CFG nodes.
Side-effecting of globals right after initialization.
Considers offsets for region accesses.
For types that have only one value.
No Additional ItemsUse implicit forward propagation instead of the demand driven approach.
volatile and extern keywords set variables permanently to top
Ensures analyses that no threads are created.
Set globals permanently to top.
Global variables that should be handled flow-sensitively when using earlyglobs.
No Additional ItemsGlobal variables that should not be invalidated. This assures the analysis that such globals are only modified through known code
No Additional ItemsLocation of the g2html.jar file. If empty, then goblint executable directory is used.
List of functions that must be analyzed as unknown extern functions
No Additional ItemsOverwrite narrow a b = a
Only keep values for basic blocks instead of for every node. Should take longer but need less space.
Only generate one 'a[any_index] = x' for all assignments a[...] = x for a global array a[n].
Architecture for analysis, currently for witness
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).
Path to C preprocessor (cpp) to use. If empty, then automatically searched.
Sets the unrolling factor for the loopUnrollingVisitor.
Hide standard extern globals (e.g. stdout
) from cluttering local states.
Abstract reachability graph (ARG) options
No Additional PropertiesConstruct ARG.
ARG output as .dot file
No Additional PropertiesARG .dot file output path. Disabled if empty.
Which ARG node labels to use? node/empty
Debugging options
No Additional PropertiesLogging level.
Collect and output timing information.
Filename for Trace Event Format (TEF) output. Disabled if empty.
Also print the context of solver variables.
Dumps the results to the given path
Where to dump cil output
Printer to use for justcil: default, or clean (excludes line directives and builtin declarations).
Stop solver after this time. 0 means no timeout. Supports optional units h, m, s. E.g. 1m6s = 01m06s = 66; 6h = 66060.
Interval in seconds to print statistics while solving. Set to 0 to deactivate.
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).
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).
Used for debugging. Prints out a symbol on solving a rhs.
Print the widening points after solving (does not include the removed wpoints during solving by the slr solvers). Currently only implemented in: slr*, td3.
Turn slicer on or off.
How deep function stack do we analyze.
Limit for number of widenings per node (0 = no limit).
Keep warnings for different contexts apart (currently only done for asserts).
Only output warnings for assertions that have an unexpected result (no comment, comment FAIL, comment UNKNOWN)
Test domain properties
Output dot files for CIL CFGs.
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
Should the analysis print information on the encountered TIDs
Should the analysis print information on which globals are protected by which mutex?
Should the analysis call Check.checkFile after creating the CFG (helpful to verify that transformations respect CIL's invariants.
Output abstract values, etc. with full internal details, without readability-oriented simplifications.
Output loop iteration bounds for terminating loops when termination analysis is activated.
Filtering of warnings
No Additional PropertiesAssert messages
undefined behavior warnings
function call warnings
integer (Overflow, Divbyzero) warnings
float warnings
Cast (Type_mismatch(bug) warnings
Race warnings
Deadlock warnings
Dead code warnings
Analyzer messages
Unsoundness messages
Imprecision messages
Witness messages
Program messages
Non-Termination warning
Unknown (of string) warnings
Error severity messages
Warning severity messages
Info severity messages
Debug severity messages
Success severity messages
Quote code in message output.
Races with confidence at least threshold are warnings, lower are infos.
Output messages in deterministic order. Useful for cram testing.
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.
Remove widening points after narrowing phase. Enables a form of local restarting which increases precision of nested loops.
Skip evaluation of RHS if all dependencies are unchanged - INCOMPATIBLE WITH RESTARTING
Restart wpoint to bot when (re-)detected. Allows incremental to avoid reusing and republishing imprecise local values due to globals (which get restarted).
Restart wpoint only on first detection. Useful for incremental loading.
Check TD3 data structure invariants
How many times SLR4 is allowed to switch from restarting iteration to increasing iteration.
Output GraphML witness
GraphML witness output path
Which witness node IDs to use? node/enumerate
Try to minimize the witness
Try to undo CIL control flow transformations in witness
Construct stacktrace-based witness nodes
Output witness for unknown result
Emit invariants at loop heads
Emit invariants after mutex locking
Emit invariants at all other locations
Split conjunctive invariant to multiple invariants
Only emit invariants for locally accessed variables
Whether to dump assertions about all local variables or limitting it to modified ones where possible.
Emit exact invariants. They are useless for unassuming.
Emit inexact invariants matching type bounds.
OCaml Str regexes for variables to exclude from invariants.
No Additional ItemsEmit invariants for local variables under the assumption they are always in scope within their function.
Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.
Emit invariants with typedef-ed types (e.g. in casts). Our validator cannot parse these.
Emit flow-insensitive invariants as location invariants at certain locations.
Output YAML witness
YAML witness format version
YAML witness entry types to output/input.
No Additional ItemsYAML witness invariant types to output/input.
No Additional ItemsYAML witness output path
YAML witness input path
Fail YAML witness validation if there's an error/unsupported/disabled entry.
YAML witness input path
YAML witness certificate output path