Skip to content

Latest commit

 

History

History
34 lines (32 loc) · 3.13 KB

options.md

File metadata and controls

34 lines (32 loc) · 3.13 KB
Raw

Predator plug-in options

For the GCC-plugin, use with the prefix -fplugin-arg-libsl. Default option in bold.

Options Description
-help Help
-verbose=<uint> Turn on verbose mode
-pid-file=<file> Write PID of self to <file>
-preserve-ec Do not affect the exit code
-dry-run Do not run the analysis
-dump-pp[=<file>] Dump linearised CL code
-dump-types Dump also type info
-gen-dot[=<file>] Generate CFGs
-type-dot=<file> Generate type graphs
-args=<peer-args> Arguments given to the analyser (see below)
Peer arguments Description
track_uninit Report usage of uninitialised values
oom Simulate possible shortage of memory (malloc can fail)
no_error_recovery No error recovery, stop the analysis as soon as an error is detected
memleak_is_error Treat memory leaks as an error
exit_leaks Report memory leaks while executing a no-return function
verifier_error_is_error Treat reaching of __VERIFIER_error() as an error
error_label:<string> Treat reaching of the given label as an error
int_arithmetic_limit:<uint> The highest integer number Predator can count to
allow_cyclic_trace_graph Create a node with two parents on entailment
forbid_heap_replace Do not replace a previously tracked node if en- tailed by a new one
allow_three_way_join[:<uint>] Using the general join of possibly incomparable SMGs (so-called three-way join)
  1. never
  2. only when joining nested sub-heaps
  3. also when joining SPCs if considered useful
  4. always
join_on_loop_edges_only[:<int>]
  1. never join, never check for entailment, always check for isomorphism
  2. join SPCs on each basic block entry
  3. join only when traversing a loop-closing edge, entailment otherwise
  4. join only when traversing a loop-closing edge, isomorphism otherwise
  5. same as 2 but skips the isomorphism check if possible
state_live_ordering[:<uint>] On the fly ordering of SPCs to be processed
  1. do not try to optimise the order of heaps
  2. reorder heaps when joining
  3. reorder heaps when creating their union (list of SMGs) too
no_plot Do not generate graphs (ignore all calls of __sl_plot*() and __VERIFIER_plot())
dump_fixed_point Dump SPCs of the obtained fixed-point
detect_containers Detect low-level implementations of high-level list containers and operations over them (such as various initialisers, iterators, etc.)