Command line Options

This document explains how to use the command line options of TrustInSoft Analyzer and their behavior.

To avoid manipulating too many command line options, Configuration files can be used.

Some Environment Variables may also be used to configure some elements of the behavior.

Evaluation order

Every command line options are evaluated from left to right.

TrustInSoft Analyzer starts the analyses (parsing files, running Value Analysis, …) once the command line has been fully evaluated or if a Sequencing options has been encountered.

A same option can be given several times during the same sequence and the behavior depends on the type of this option.

Caution

A few command line options are evaluated before any other ones, such as -load, -load-script, -tis-config-select, …

These options are exceptions since their associated action (resp. value) is expected to be run (resp. computed) before any other command line.

Sequencing options

Sequencing options can be used to perform several times the analyses with the same TrustInSoft Analyzer process.

The main sequencing option is -then. Every option given before -then is kept for the next sequences.

For instance, the two following commands are equivalent:

tis-analyzer file.c -val -slevel 10 -then another_file.c -val -slevel 10 -slevel 20
tis-analyzer file.c -val -slevel 10 -then another_file.c -slevel 20

The above commands do:

  • Parse file.c and run the Value Analysis with a slevel of 10
  • Then parse another_file.c and run the Value Analysis with a slevel of 20

On a new sequence, the parsing or analyses are done again only if it is necessary;

  • files are parsed only if the list of files changes or if a command line option impacting the parsing of these files changes
  • an analysis (Value Analysis, WP, …) is only done again:
    • if a command line option impacting the analysis changes
    • if files has been parsed again or a dependent analysis has been done again in this new sequence

For instance,

tis-analyzer file.c -val -slevel 10 -then -slevel 20

The above command does:

  • Parse file.c and run the Value Analysis with a slevel of 10
  • Then run again the Value Analysis with a slevel of 20

In this example, it allows to run twice the Value Analysis with different tuning options without parsing again file.c.

Tip

The other sequencing options are: -then-last, -then-replace and -then-on which are relevant only after running a program transformer operation (such as the Slicing operation).

Meta-options

A meta-option is a command line option that sets several other command line options (such as -tis-config-load, -val-profile or -language-mode).

The behavior is the same one as if the command line options set by the meta-option were written at the same place where the meta-option is on the command line.

For instance, with the following configuration file:

{ "slevel": 20,
  "cpp-extra-args": [ "-I include/" ] }

the two following commands are equivalent:

tis-analyzer test.c -tis-config-load tis.config -then -slevel 10
tis-analyzer test.c -slevel 20 -cpp-extra-args="-I include/" -then -slevel 10

Tip

Reminder: some fields in a configuration files cannot be translated to a command line option.

In some cases, the usage of a configuration file is unavoidable.

Option types

The type of an option impacts:

  • whether the option takes an argument
  • whether some characters are reserved in the argument for a particular semantic
  • the value of the option if this option is given several times in a same sequence

The type of each option is indicated in the List of options.

Simple type options

Simple type options refer to options with a boolean, integer or string type.

If such an option is given several times in a same sequence, the value is overwritten and only the rightmost value is kept at the end of the evaluation.

Caution

If the argument of an option starts with -, the argument will be interpreted as an option name instead of an argument.

To avoid this behavior, use the syntax -option-name=value instead of -option-name value.

Example:

tis-analyzer -cpp-extra-args="-I include -DFOO"

Boolean type options

Boolean options do not take any argument: using the option sets its value to true.

Most of boolean options have also an opposite option, and when used the option sets its value to false. The default name of the opposite option is -no-<option_name>. Some boolean options have no opposite option, which means their default value is false and once used, the option cannot be unset.

Information about the opposite option is indicated in the List of options for boolean type options.

Integer type options

Integer options take one argument which should be a positive or negative integer. Floating numbers are considered as a string and are included in string type options.

Some integer options accept only a restricted range of values. In this case, the range is indicated in the List of options.

String type options

String options take one argument always interpreted as a string (even if the value represents number).

Some string options accept only a restricted set of values. In this case, the list of accepted values is indicated in the List of options.

List type options

List options can take one or several strings as argument.

If such options are given several times, the values are appended to any previous ones, by keeping the evaluation order (from left to right) for the final value of the option.

Several values can also be given in a single argument. In this case, the comma , character is used as a separator.

For instance, the two following command lines are equivalent:

tis-analyzer -compilation-database directory1 -compilation-database directory2
tis-analyzer -compilation-database directory1,directory2

Caution

If the argument contains a comma , in its value, the comma should be escaped with a backslash \.

Example:

tis-analyzer -cpp-extra-args="-D MY_REALLOC(a\,b)=realloc(a\,b)"

Set type options

Set options can take one or several string arguments.

If such options are given several times, the values are accumulated in a set, which cannot contains duplicates and the evaluation order is not kept.

Several values can also be given in a single argument. In this case, the comma , character is used as a separator.

For instance, the three following command lines are equivalent:

tis-analyzer -val-use-spec main -val-use-spec f
tis-analyzer -val-use-spec main,f
tis-analyzer -val-use-spec f,main

Set options also allows the usage of the -<value> syntax to remove the given <value> from the set.

Example:

tis-analyzer -val-use-spec main,f,g -val-use-spec h,-f
// The -val-use-spec option is only enabled for the "main", "g",
// and "h" functions.

Caution

If the argument contains a comma , in its value, the comma should be escaped with a backslash \.

Similarly, if the real value begins with a - and should not be interpreted as the syntax to remove a value, the - should be escaped with a backslash \.

Example:

tis-analyzer -a-set-option 'a\,a,b,\-b'
// The value of the -a-set-option is
//   { "a,a"; "b"; "-b" }

Set options allows the usage of Categories. In this case, the allowed categories are indicated in the List of options.

Tip

The -@all keyword is always allowed to remove all values from the set, even if the @all category is not available for the option.

Map type options

Map options can take one or several arguments. Each argument is a pair of a key and a value, separated with a colon :. Keys and values are strings.

Caution

The two characters :: are not considered as separators, to easily write C++ identifiers.

If such options are given several times, the new bindings (the key-value association) are accumulated to the map with any previous ones. If a same key is given twice, only the latest value is kept.

Several bindings can also be given in a single argument. In this case, the comma , character is used as a separator.

For instance, the two following command lines are equivalent:

tis-analyzer -slevel-function main:10 -slevel-function f:5
tis-analyzer -slevel-function main:10,f:5

Set options also allows the usage of the -<value> syntax to remove the given <value> from the set.

Example:

tis-analyzer -slevel-function main:10,f:5 -slevel-function=-main
// The -slevel-function option is only enabled for the "f" function.

Caution

If a key or a value of an argument contains a comma ,, the comma should be escaped with a backslash \.

Similarly, if the key begins with a - and should not be interpreted as the syntax to remove a binding, the - should be escaped with a backslash \.

If a key contains a colon :, the colon should be escaped with a backslash \. However, there is no need to escape colon in values.

Example:

tis-analyzer -a-map-option 'a\,a\:a:a,b:0,\-b:-1'
// The value of the -a-map-option is
//   { "a,a:a" -> "a:a"; "b" -> "0"; "-b" -> "-1" }

Map options allows the usage of Categories. In this case, the allowed categories are indicated in the List of options.

Tip

The -@all keyword is always allowed to remove all values from the set, even if the @all category is not available for the option.

Categories

Categories are a feature available only for Set type options and Map type options.

This feature allows the usage of the @<name> (and -@<name>) syntax to replace @<name> by several values already defined in TrustInSoft Analyzer.

The available categories (and their names) are different for each option supporting categories and are indicated in the List of options.

For instance, if the category abc defining three values a, b and c is available for the option -my-opt, then the two following command lines are equivalent:

tis-analyzer -my-opt a,b,c
tis-analyzer -my-opt @abc

Also, using -@<name> is equivalent to remove all values defined by the category from the option. For instance, the two following command lines are equivalent:

tis-analyzer -my-opt a,b,c,d,e,-a,-b,-c
tis-analyzer -my-opt a,b,c,d,e,-@abc

Tip

The most well-known used category is the @all, allowing to substitute this word by every possible values for this option.

Also, -@all is a special keyword allowing the remove any values from a set or a map even if the @all is not available for the option.

For instance, the following command line allows to enable the -val-slevel-merge-after-loop for every function of the analyzed program except f:

tis-analyzer -val-slevel-merge-after-loop @all,-f

On the contrary, using -@all will remove all values of the list/set:

tis-analyzer -tis-config-load tis.config -val-slevel-merge-after-loop=-@all,f
// Load the given configuration files and ensures that
// -val-slevel-merge-after-loop is only enabled for "f"
// whatever the configuration files contains.

Caution

If the value of a set or a key of a map begins with a @ and should not be interpreted as the category syntax, the @ should be escaped with a backslash \.

Example:

tis-analyzer -a-set-option "@all,-\@b"
// Enable the -a-set-option for all possible values except for
// the value "@b"

List of options

This is the list of all the available options in TrustInSoft Analyzer.

For each of option, it indicates:

–help
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • display a general help
–list-plugins
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • display a general help
-absolute-address
  • Provided by: Kernel :: Analysis Options
  • Type: map
  • Default: <none>
  • Categories: <none>
  • specify absolute addresses constraints for some global variables. A precise addresses is an integer in decimal, hexadecimal (0x, 0X), octal (0o) or binary (0b) notation. A range may be specified by ‘[<min>..<max>]’ where <min> must be smaller than <max>. Moreover, an optional alignment constraint may be added. Example: ‘[0xA000 .. 0xB000],0%4’.
-absolute-valid-range
  • Provided by: Kernel :: Analysis Options
  • Type: string
  • Default: <none>
  • min and max must be integers in decimal, hexadecimal (0x, 0X), octal (0o) or binary (0b) notation and fit in 64 bits. Assume that that all absolute addresses outside of the [min-max] range are invalid. In the absence of this option, all absolute addresses are assumed to be invalid
-access-path
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-access-path
  • force the access path information to be computed
-acsl-Idir
  • Provided by: ACSL importer
  • Type: list
  • Default: <none>
  • directory for searching ACSL files to include
-acsl-addon-ensures-and-exits
  • Provided by: ACSL importer
  • Type: boolean
  • Default: false
  • Opposite option: -no-acsl-addon-ensures-and-exits
  • adds ensures_and_exits extension clause
-acsl-addon-integer-cast
  • Provided by: ACSL importer
  • Type: boolean
  • Default: false
  • Opposite option: -no-acsl-addon-integer-cast
  • allows and explicits casts from integer to C integral types
-acsl-import
  • Provided by: ACSL importer
  • Type: list
  • Default: <none>
  • ACSL files to import
-acsl-importer-debug
  • Provided by: ACSL importer :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in ACSL importer
-acsl-importer-help
  • Provided by: ACSL importer :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in ACSL importer
-acsl-importer-msg-key
  • Provided by: ACSL importer :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -acsl-importer-msg-key help to get a list of available categories, and * to enable all categories
-acsl-importer-verbose
  • Provided by: ACSL importer :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in ACSL importer
-acsl-run
  • Provided by: ACSL importer
  • Type: boolean
  • Default: true
  • Opposite option: -no-acsl-run
  • runs the plugin otherwise, just configure the parameters
-acsl-ulevel-spec
  • Provided by: ACSL importer
  • Type: map
  • Default: <none>
  • Categories: <none>
  • an unrolling specification <m@f:tag@n> adds a ‘loop pragma UNROLL “tag”, <n>;’ to the loop of the function <f> of occurrence <m>. An unrolling specification <c@f:tag@n> adds a ‘loop pragma UNROLL “tag”, <n>;’ to all loops of category <c> of the function <f> where allowed loop categories are: ‘while’, ‘for’ and ‘do-while’. The specification is considered as a set of elementary specifications: spec1,…,specs. Categories, function names and loop occurrence numbers can be omitted. The priority ordering used for choosing the (“tag”, unrolling value <n>) pair is: m@f:tag@n > c@f:tag@n > f:tag@n > c:tag@n > :tag@n. The default value for optional tags is the empty string which leads to add a loop pragmas without tags. Nothing is done for loops having already a clause ‘loop pragma UNROLL …’.
-acsl-unroll-loop-conditions
  • Provided by: ACSL importer
  • Type: boolean
  • Default: false
  • Opposite option: -no-acsl-unroll-loop-conditions
  • unrolls statements related to loop conditions
-acsl-version
  • Provided by: ACSL importer
  • Type: boolean
  • Default: false
  • Opposite option: -no-acsl-version
  • prints plugin version
-acsl-warn-integer-cast
  • Provided by: ACSL importer
  • Type: boolean
  • Default: true
  • Opposite option: -no-acsl-warn-integer-cast
  • emits a warning when casting an integer into a C integral type
-add-path
  • Provided by: Kernel :: Saving or Loading Data
  • Type: list
  • Default: <none>
  • Prepend directories to TIS_KERNEL_PLUGIN for loading dynamic plug-ins
-add-symbolic-path
  • Provided by: Kernel :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • When displaying file locations, replace (absolute) path by the corresponding symbolic name
-address-alignment
  • Provided by: Kernel :: Analysis Options
  • Type: integer
  • Default: 1
  • Possible values: between 1 and 65536
  • base addresses are assumed to be aligned to multiples of n
-aggreg-debug
  • Provided by: Aggregate plugin :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in aggregate plugin
-aggreg-help
  • Provided by: Aggregate plugin :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in aggregate plugin
-aggreg-html-stmts
  • Provided by: Aggregate plugin
  • Type: string
  • Default: <none>
  • export all the functions in HTML format to the ‘dirname’ directory to be used later on by tis-aggregate coverage. When the directory already exists, previously existing files are overwritten to make sure the more recent version is available.
-aggreg-msg-key
  • Provided by: Aggregate plugin :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -aggreg-msg-key help to get a list of available categories, and * to enable all categories
-aggreg-verbose
  • Provided by: Aggregate plugin :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in aggregate plugin
-aggressive-merging
  • Provided by: Kernel :: Customizing Normalization
  • Type: string
  • Default: inline
  • Possible values:both, inline, off, static
  • Attempt to merge inline and / or static functions that have been included in the sources multiple times (e.g. defined in a .h file that is included in many .c files).
-all-rounding-modes
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: false
  • Opposite option: -no-all-rounding-modes
  • Take more target FPU and compiler behaviors into account
-all-rounding-modes-constants
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: false
  • Opposite option: -no-all-rounding-modes-constants
  • Take into account the possibility of constants not being converted to the nearest representable value, or being converted to higher precision
-allow-duplication
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-allow-duplication
  • allow duplication of small blocks during normalization
-allow-left-shift-into-sign-bit
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: <none>
  • Opposite option: -no-allow-left-shift-into-sign-bit
  • Allow or disallow a left-shift of a signed integer that does not overflow the corresponding unsigned type. Setting this option overrides the semantics of << defined by ISO-C and ISO-C++
-allow-null-lt-null
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: <none>
  • Opposite option: -no-allow-null-lt-null
  • Allow or disallow comparing null pointers with relational operators. Setting this option overrides the semantics of relational operators defined by ISO-C and ISO-C++.
-allow-null-plus-zero
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: <none>
  • Opposite option: -no-allow-null-plus-zero
  • Allow or disallow adding zero to a null pointer. Setting this option overrides the semantics of additive operators defined by ISO-C and ISO-C++
-annot
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: true
  • Opposite option: -no-annot
  • read and parse annotations
-aorai-AI-off
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-AI-off
  • does not use abstract interpretation
-aorai-acceptance
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-acceptance
  • if set, considers acceptation states
-aorai-add-oper
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-add-oper
  • Adding current operation name (and statut) in pre/post conditions
-aorai-automata
  • Provided by: Aorai
  • Type: string
  • Default: <none>
  • considers the property described by the ya automata (in Ya language) from file <f>.
-aorai-buchi
  • Provided by: Aorai
  • Type: string
  • Default: <none>
  • considers the property described by the buchi automata (in Promela language) from file <f>.
-aorai-debug
  • Provided by: Aorai :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in aorai
-aorai-dot
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-dot
  • generates a dot file of the Buchi automata
-aorai-dot-sep-labels
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-dot-sep-labels
  • tells dot to not output guards directly over the edges
-aorai-help
  • Provided by: Aorai :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in aorai
-aorai-ltl
  • Provided by: Aorai
  • Type: string
  • Default: <none>
  • specifies file name for LTL property
-aorai-msg-key
  • Provided by: Aorai :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -aorai-msg-key help to get a list of available categories, and * to enable all categories
-aorai-output-c-file
  • Provided by: Aorai
  • Type: string
  • Default: <none>
  • specifies generated file name for annotated C code
-aorai-show-op-spec
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-show-op-spec
  • displays computed pre and post-condition of each operation
-aorai-simple-AI
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-simple-AI
  • use simple abstract interpretation
-aorai-simplified-auto
  • Provided by: Aorai
  • Type: boolean
  • Default: true
  • Opposite option: -aorai-raw-auto
  • If set, does not simplify automata
-aorai-spec-on
  • Provided by: Aorai
  • Type: boolean
  • Default: true
  • Opposite option: -aorai-spec-off
  • if set, does not axiomatize automata
-aorai-test
  • Provided by: Aorai
  • Type: boolean
  • Default: false
  • Opposite option: -aorai-no-test
  • Testing mode
-aorai-to-buchi
  • Provided by: Aorai
  • Type: string
  • Default: <none>
  • only generates the buchi automata (in Promela language) in file <s>
-aorai-verbose
  • Provided by: Aorai :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in aorai
-asm-contracts
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-asm-contracts
  • generate contracts for assembly code written according to gcc’s extended syntax
-asm-contracts-auto-validate
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-asm-contracts-auto-validate
  • automatically mark contracts generated from asm as valid
-big-ints-hex
  • Provided by: Kernel :: Input/Output Source Code
  • Type: integer
  • Default: -1
  • display integers larger than <max> using hexadecimal notation
-binding-auto
  • Provided by: Volatile
  • Type: boolean
  • Default: false
  • Opposite option: -no-binding-auto
  • allows automatic binding to functions from volatile type names: Rd_<type-name> and Wr_<type-name> for read and write accesses (the use of the option -volatile-msg-key=”binding” could help to guess the necessary <type-name>)
-binding-prefix
  • Provided by: Volatile
  • Type: string
  • Default: c2fc2_
  • adds <str> as prefix to function names for automatic binding
-calldeps
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-calldeps
  • force callsite-wise dependencies
-calldeps-print
  • Provided by: From analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-calldeps-print
  • print results for option -calldeps
-cfp
  • Provided by: Context From Precondition
  • Type: boolean
  • Default: false
  • Opposite option: -no-cfp
  • run the analysis
-cfp-annotate-switch
  • Provided by: Context From Precondition
  • Type: boolean
  • Default: false
  • Opposite option: -cfp-no-annotate-switch
  • generate ACSL annotations on generated switch cases
-cfp-debug
  • Provided by: Context From Precondition :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Context From Precondition
-cfp-externals
  • Provided by: Context From Precondition
  • Type: set
  • Default: <none>
  • Categories: <none>
  • name of the formal parameters of the input functions which no code is generated for
-cfp-externals-with-value
  • Provided by: Context From Precondition
  • Type: map
  • Default: <none>
  • Categories: <none>
  • Like -cfp-externals but also provide an integer value for each formal
-cfp-help
  • Provided by: Context From Precondition :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Context From Precondition
-cfp-inference
  • Provided by: Context From Precondition
  • Type: boolean
  • Default: true
  • Opposite option: -cfp-no-inference
  • automatically generate additional constraints when some preconditions are missing
-cfp-input
  • Provided by: Context From Precondition
  • Type: string
  • Default: main
  • name of the function which the context must be generated from
-cfp-msg-key
  • Provided by: Context From Precondition :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -cfp-msg-key help to get a list of available categories, and * to enable all categories
-cfp-output
  • Provided by: Context From Precondition
  • Type: string
  • Default: <none>
  • name of the function containing the generated context (if -cfp-input is “f” and -cfp-prefix is “p”, default is “pf”)
-cfp-prefix
  • Provided by: Context From Precondition
  • Type: string
  • Default: __cfp_
  • prefix used to generate variable names
-cfp-project
  • Provided by: Context From Precondition
  • Type: string
  • Default: cfp
  • name of the generated project
-cfp-session
  • Provided by: Context From Precondition
  • Type: string
  • Default: <none>
  • set the plug-in session directory to <dir>
-cfp-verbose
  • Provided by: Context From Precondition :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Context From Precondition
-cfp-version
  • Provided by: Context From Precondition :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -cfp-no-version
  • version of the plug-in.
-cg
  • Provided by: Callgraph
  • Type: string
  • Default: <none>
  • dump the callgraph to the file <filename> in dot format
-cg-debug
  • Provided by: Callgraph :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in callgraph
-cg-help
  • Provided by: Callgraph :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in callgraph
-cg-init-func
  • Provided by: Callgraph
  • Type: set
  • Default: <none>
  • Categories: all
  • use the given set of functions as root services for the callgraph
-cg-msg-key
  • Provided by: Callgraph :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -cg-msg-key help to get a list of available categories, and * to enable all categories
-cg-services
  • Provided by: Callgraph
  • Type: boolean
  • Default: true
  • Opposite option: -cg-no-services
  • compute and display the services from the callgraph
-cg-uncalled
  • Provided by: Callgraph
  • Type: boolean
  • Default: true
  • Opposite option: -cg-no-uncalled
  • add the uncalled functions to the callgraph (the main function is always added anyway)
-cg-uncalled-leaf
  • Provided by: Callgraph
  • Type: boolean
  • Default: false
  • Opposite option: -cg-no-uncalled-leaf
  • add to the callgraph the uncalled functions that do not call themselves any function
-cg-verbose
  • Provided by: Callgraph :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in callgraph
-check
  • Provided by: Kernel :: Checks
  • Type: boolean
  • Default: false
  • Opposite option: -no-check
  • performs consistency checks over the Abstract Syntax Tree
-codpds
  • Provided by: Pdg :: Output
  • Type: boolean
  • Default: false
  • Opposite option: -no-codpds
  • force option -pdg-print to show the co-dependencies rather than the dependencies
-collapse-call-cast
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-collapse-call-cast
  • Allow some implicit casts between returned value of a function and the lvalue it is assigned to.
-colors
  • Provided by: Kernel :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-colors
  • enable colors in output messages
-compilation-database
  • Provided by: Kernel
  • Type: list
  • Default: <none>
  • Fill a database with data of the given JSON files according to format described in https://clang.llvm.org/docs/JSONCompilationDatabase.html . If a directory is given, then all ‘compile_commands.json’ files in this directory and its sub-directories will be scanned. This database will be used to add compile options for the preprocessor for the list of files to parse. Any compile options added from this database is added before any other compile options given with the -cpp-extra-args option.
-config
  • Provided by: Kernel :: Saving or Loading Data
  • Type: string
  • Default: <none>
  • directory in which configuration files are searched
-const-readonly
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: true
  • Opposite option: -const-writable
  • variables with the ‘const’ qualifier must be actually constant
-constfold
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-constfold
  • fold all constant expressions in the code before analysis
-context-depth
  • Provided by: Value analysis :: Initial Context
  • Type: integer
  • Default: 2
  • use <n> as the depth of the default context for value analysis.
-context-uninitialized-extern
  • Provided by: Value analysis :: Initial Context
  • Type: boolean
  • Default: false
  • Opposite option: -no-context-uninitialized-extern
  • Consider that the declared and not defined global variables are not initialized.
-context-valid-pointers
  • Provided by: Value analysis :: Initial Context
  • Type: boolean
  • Default: false
  • Opposite option: -no-context-valid-pointers
  • only allocate valid pointers until context-depth, and then use NULL.
-context-width
  • Provided by: Value analysis :: Initial Context
  • Type: integer
  • Default: 2
  • Possible values: integers >= 1
  • use <n> as the width of the default context for value analysis.
-continue-annot-error
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: false
  • Opposite option: -no-continue-annot-error
  • When an annotation fails to type-check, emit a warning and discard the annotation instead of generating an error (errors in C are still fatal)
-copy
  • Provided by: Kernel :: Checks
  • Type: boolean
  • Default: false
  • Opposite option: -no-copy
  • always perform a copy of the original AST before analysis begin
-cpp-command
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: clang -C -E -nostdinc
  • <cmd> is used to build the preprocessing command. Default to $CPP environment variable or else “gcc -C -E -I.”. If unset, the command is built as follows: CPP -o <preprocessed file> <source file> %1 and %2 can be used into CPP string to mark the position of <source file> and <preprocessed file> respectively
-cpp-command-file
  • Provided by: Kernel :: Parsing
  • Type: map
  • Default: <none>
  • Categories: <none>
  • Same as -cpp-command but set a preprocessing command per file. See also -compilation-database option for more complex builds. If a file has a preprocessing command given in this option, then the global preprocessing command given with -cpp-command is ignored. Any file not listed in this option uses the global preprocessing command.
-cpp-extra-args
  • Provided by: Kernel :: Parsing
  • Type: list
  • Default: -ITIS_KERNEL_SHARE/mt, -D__TRUSTINSOFT_ANALYZER__, -D__TRUSTINSOFT_HELPER__, -D__TRUSTINSOFT_LABEL__, -D__TRUSTINSOFT_BUGFIX__, -D__TRUSTINSOFT_TMPBUG__
  • additional arguments passed to the preprocessor while preprocessing the C code but not while preprocessing annotations
-cpp-extra-args-file
  • Provided by: Kernel :: Parsing
  • Type: map
  • Default: <none>
  • Categories: <none>
  • Same as -cpp-extra-args but the additional arguments passed to the preprocessor only impact the associated file. Arguments given by this option are passed after the ones of the -cpp-extra-args option, except in the following case: if the first character of the value is ‘@’, then any previous additional arguments given by the -cpp-extra-args and -compilation-database options are removed (only arguments given by -cpp-command persist). Hence, a leading ‘@’ character allows to overwrite any previous arguments to keep only the ones given by this option. See also -compilation-database option for more complex builds.
-cpp-gnu-like
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: true
  • Opposite option: -no-cpp-gnu-like
  • indicates that a custom pre-processor (see option -cpp-command) accepts the same set of options as GNU cpp. Set it to false if you have pre-processing issues with a custom pre-processor.
-cpp-target-option
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: true
  • Opposite option: -no-cpp-target-option
  • indicates that a custom pre-processor (see option -cpp-command) accepts the -target option. Set it to false if you have pre-processing issues with a custom pre-processor.
-custom-annot-char
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: <none>
  • use a custom character <c> for starting ACSL annotations
-cxx-annot
  • Provided by: CXX
  • Type: boolean
  • Default: true
  • Opposite option: -no-cxx-annot
  • Parse ACSL++ annotations.
-cxx-cache-all
  • Provided by: CXX :: Cache management
  • Type: boolean
  • Default: false
  • Opposite option: -no-cxx-cache-all
  • Force persistent caching of all analyzed files. It is the responsibility of the user to check that the file does not change between successive calls to the analyzer.
-cxx-clean-cache-locks
  • Provided by: CXX :: Cache management
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • Release the locks on cached files and exit.
-cxx-cpp-extra-args
  • Provided by: CXX
  • Type: list
  • Default: <none>
  • additional arguments passed to the preprocessor while preprocessing the C++ code but not while preprocessing annotations
-cxx-debug
  • Provided by: CXX :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in CXX
-cxx-debug-fir
  • Provided by: CXX
  • Type: string
  • Default: nnnnnn
  • abcdef where a is before odr cache optimization, b is before class declaration completion, c is before lift, d is before reorder, e is before class definition completion, and f is the final result.
-cxx-debug-graph
  • Provided by: CXX
  • Type: string
  • Default: <none>
  • dump a <template>.svg file with its <template>.dot file and a <template>.txt file with id-name associations
-cxx-demangling-full
  • Provided by: CXX
  • Type: boolean
  • Default: false
  • Opposite option: -cxx-no-demangling-full
  • displays identifiers with their full C++ name
-cxx-demangling-short
  • Provided by: CXX
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • displays identifiers with their C++ short name (without qualifiers)
-cxx-elide-constructors
  • Provided by: CXX
  • Type: boolean
  • Default: true
  • Opposite option: -no-cxx-elide-constructors
  • Elide copy constructor calls whenever possible.
-cxx-evaluate-constexpr
  • Provided by: CXX
  • Type: boolean
  • Default: true
  • Opposite option: -no-cxx-evaluate-constexpr
  • Evaluate constexpr expressions.
-cxx-filt
  • Provided by: CXX
  • Type: string
  • Default: <none>
  • print the unmangled version of <name> and exit.
-cxx-frontend
  • Provided by: CXX
  • Type: string
  • Default: tis-cxxfrontend
  • use <cmd> as the parsing command. Defaults to tis-cxxfrontend
-cxx-generate-contracts
  • Provided by: CXX
  • Type: boolean
  • Default: true
  • Opposite option: -no-cxx-generate-contracts
  • Generate function contracts for class methods whenever possible.
-cxx-generate-empty-constructors
  • Provided by: CXX
  • Type: boolean
  • Default: false
  • Opposite option: -no-cxx-generate-empty-constructors
  • Produce default, empty bodies for missing constructors.
-cxx-help
  • Provided by: CXX :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in CXX
-cxx-keep-mangling
  • Provided by: CXX
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • displays identifiers with their mangled name
-cxx-msg-key
  • Provided by: CXX :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -cxx-msg-key help to get a list of available categories, and * to enable all categories
-cxx-odr-optimize
  • Provided by: CXX
  • Type: boolean
  • Default: true
  • Opposite option: -no-cxx-odr-optimize
  • Replace ODR-duplicate definitions by declarations.
-cxx-pass-by-value
  • Provided by: CXX
  • Type: list
  • Default: <none>
  • Force pass-by-value for the type <name> when argument passing is unknown.
-cxx-precompile
  • Provided by: CXX :: Cache management
  • Type: boolean
  • Default: false
  • Opposite option: -no-cxx-precompile
  • Precompile C++ file.
-cxx-precompile-path
  • Provided by: CXX :: Cache management
  • Type: list
  • Default: <none>
  • paths where to look for C++ precompile candidates.
-cxx-runtime
  • Provided by: CXX
  • Type: boolean
  • Default: false
  • Opposite option: -no-cxx-runtime
  • Adds runtime files for the STL.
-cxx-std
  • Provided by: CXX
  • Type: string
  • Default: c++11
  • Possible values:c++03, c++0x, c++11, c++14, c++17, c++1y, c++1z, c++20, c++2a, c++98, gnu++03, gnu++0x, gnu++11, gnu++14, gnu++17, gnu++1y, gnu++1z, gnu++20, gnu++2a, gnu++98
  • follow <std> as the C++ standard.
-cxx-stdinc
  • Provided by: CXX
  • Type: boolean
  • Default: true
  • Opposite option: -no-cxx-stdinc
  • Adds TrustInSoft Kernel standard headers for C and C++ in include path.
-cxx-verbose
  • Provided by: CXX :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in CXX
-dead-bk-skip-tis-dead
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-bk-skip-tis-dead
  • If all the statements in a dead block are in blocks marked with __blockattribute__(__tis_dead__), do not report this dead block in the results.
-dead-bk-summary
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-bk-summary
  • Print a summary about dead code blocks in reachable functions in CSV format.
-dead-bk-with-defs
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-bk-with-defs
  • Print the origin of the sub-expressions of the tests (only if -dead-bk-with-tests and also needs the -whole-program-graph option).
-dead-bk-with-subexp
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-bk-with-subexp
  • Print the values of the sub-expressions of the tests (only if -dead-bk-with-tests).
-dead-bk-with-tests
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-bk-with-tests
  • Print the test expressions of the dead blocks.
-dead-bk-with-tis-dead
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-bk-with-tis-dead
  • Print information about the blocks marked with __blockattribute__(__tis_dead__).
-dead-compute
  • Provided by: Info :: Dead code
  • Type: boolean
  • Default: false
  • Opposite option: -no-dead-compute
  • Print information about dead code. See other ‘-dead-xxx’ options with -info-help. to tune the details of the computation.
-dead-functions
  • Provided by: Info :: Dead code
  • Type: set
  • Default: <none>
  • Categories: all
  • Name of the functions to examine. Examine all of them by default.
-dead-json
  • Provided by: Info :: Dead code
  • Type: string
  • Default: <none>
  • Compute the same results than the -dead-compute option, and print them to the given file using the JSON format.
-dead-justification
  • Provided by: Info :: Dead code
  • Type: string
  • Default: <none>
  • generate a justification file to be used with tis-aggregate. Not available when using the -dead-functions option.
-debug
  • Provided by: Kernel :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • general level of debug
-deps
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-deps
  • force dependencies display
-deps-print
  • Provided by: From analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-deps-print
  • print results for option -deps
-deps-show-progress
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-deps-show-progress
  • Show progression messages during analysis
-deref
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-deref
  • force deref computation (undocumented)
-deterministic
  • Provided by: Kernel :: Project-related Options
  • Type: boolean
  • Default: true
  • Opposite option: <none>
-disable-constructors
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -enable-constructors
  • disable call to functions with the constructor attribute at the beginning of the entry point.
-disable-exn
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-disable-exn
  • disables the handling of exceptions completely. It transforms throw into calls to tis_std_terminate and removes all try/catch statements. Input source languages that have an exception mechanism may set this option automatically.
-dot-postdom
  • Provided by: Postdominators
  • Type: string
  • Default: <none>
  • put the postdominators of function <f> in basename.f.dot
-dump-cmdline
  • Provided by: Kernel
  • Type: boolean
  • Default: false
  • Opposite option: -no-dump-cmdline
  • Print the full command line after resolving all the options and exit as soon as possible. Useful when meta-options are used to set other options.
-dump-cmdline-output
  • Provided by: Kernel
  • Type: string
  • Default: <none>
  • Print the full command line given by the -dump-cmdline option into the given filename.
-dump-dependencies
  • Provided by: Kernel :: Getting Information
  • Type: string
  • Default: <none>
-enomem-value
  • Provided by: Kernel :: Analysis Options
  • Type: integer
  • Default: 75
  • The ENOMEM errno value. This value must match the value defined in the header files used for the analysis.
-enum-restriction
  • Provided by: Kernel :: Analysis Options
  • Type: string
  • Default: loose
  • Possible values:loose, strict, stricter
  • set the kinds of restriction for enum values. Allowed values are “loose”, “strict”, and “stricter”.
-enums
  • Provided by: Kernel :: Customizing Normalization
  • Type: string
  • Default: gcc-enums
  • Possible values:gcc-enums, gcc-short-enums, int
  • Specify how enumerated types are represented.
-erange-value
  • Provided by: Kernel :: Analysis Options
  • Type: integer
  • Default: 3
  • The ERANGE errno value. This value must match the value defined in the header files used for the analysis.
-experimental-mem-deps
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-experimental-mem-deps
  • experimental
-experimental-mem-deps-print
  • Provided by: From analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-experimental-mem-deps-print
  • print results for option -experimental-mem-deps
-experimental-path-deps
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-experimental-path-deps
  • experimental
-experimental-path-deps-print
  • Provided by: From analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-experimental-path-deps-print
  • print results for option -experimental-path-deps
-fct-pdg
  • Provided by: Pdg
  • Type: set
  • Default: <none>
  • Categories: all
  • build the dependence graph for the specified function
-findocc-debug
  • Provided by: Find Occurrence :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Find Occurrence
-findocc-help
  • Provided by: Find Occurrence :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Find Occurrence
-findocc-msg-key
  • Provided by: Find Occurrence :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -findocc-msg-key help to get a list of available categories, and * to enable all categories
-findocc-verbose
  • Provided by: Find Occurrence :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Find Occurrence
-float-hex
  • Provided by: Kernel :: Input/Output Source Code
  • Type: boolean
  • Default: false
  • Opposite option: -no-float-hex
  • display floats as hexadecimal
-float-normal
  • Provided by: Kernel :: Input/Output Source Code
  • Type: boolean
  • Default: false
  • Opposite option: -no-float-normal
  • display floats with internal routine
-float-relative
  • Provided by: Kernel :: Input/Output Source Code
  • Type: boolean
  • Default: false
  • Opposite option: -no-float-relative
  • display float intervals as [lower_bound ++ width]
-force-rl-arg-eval
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-force-rl-arg-eval
  • Force right to left evaluation order for arguments of function calls
-from-compute
  • Provided by: From analysis
  • Type: boolean
  • Default: true
  • Opposite option: -from-no-compute
  • compute the dependencies
-from-debug
  • Provided by: From analysis :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in from analysis
-from-help
  • Provided by: From analysis :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in from analysis
-from-msg-key
  • Provided by: From analysis :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -from-msg-key help to get a list of available categories, and * to enable all categories
-from-verbose
  • Provided by: From analysis :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in from analysis
-from-verify-assigns
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -from-no-verify-assigns
  • verification of assigns/from clauses for functions with bodies. Implies -calldeps
-fs
  • Provided by: Tis-mkfs
  • Type: string
  • Default: <none>
  • Provide the source file generated by tis-mkfs that gives a model of the filesystem to be used. The default behavior is to analyze the application with an empty filesystem. To disable this default behavior and use no filesystem model at all, use the -no-fs option.
-fs-error
  • Provided by: Tis-mkfs
  • Type: boolean
  • Default: true
  • Opposite option: -no-fs-error
  • Extend the tis-mkfs model of the filesystem to include errors coming from the underlying system behavior. The value of this option is only meaningful when using a filesystem model (see -fs option).
-fun-inout-print
  • Provided by: Inout :: Output Messages
  • Type: string
  • Default: <none>
  • Prints in a json format, the in values of the listed functions (f1,…,fn) into the given filename (file)
-gasgn
  • Provided by: Assigns generator
  • Type: boolean
  • Default: false
  • Opposite option: -no-gasgn
  • assigns generation on all functions.
-gasgn-confidence
  • Provided by: Assigns generator
  • Type: integer
  • Default: 1
  • Possible values: between 0 and 2
  • tune the computation according to the wanted confidence level. 0: compute as much as possible. No matter if the result is not valid; 1: the result is valid if the no-alias hypothesis holds (default); 2: the result is always valid.
-gasgn-debug
  • Provided by: Assigns generator :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Assigns generator
-gasgn-fct
  • Provided by: Assigns generator
  • Type: set
  • Default: <none>
  • Categories: all
  • generation only for the selected functions.
-gasgn-help
  • Provided by: Assigns generator :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Assigns generator
-gasgn-libc
  • Provided by: Assigns generator
  • Type: boolean
  • Default: false
  • Opposite option: -gasgn-no-libc
  • assigns generation also on libc functions.
-gasgn-msg-key
  • Provided by: Assigns generator :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -gasgn-msg-key help to get a list of available categories, and * to enable all categories
-gasgn-verbose
  • Provided by: Assigns generator :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Assigns generator
-gasgn-version
  • Provided by: Assigns generator
  • Type: boolean
  • Default: false
  • Opposite option: -gasgn-no-version
  • print assigns generation plug-in version.
-graphdeps
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-graphdeps
  • compute callwise dependencies from the Value result graph
-hcg
  • Provided by: Heuristiccallgraph
  • Type: boolean
  • Default: false
  • Opposite option: -no-hcg
  • activate metrics computation
-hcg-debug
  • Provided by: Heuristiccallgraph :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in heuristiccallgraph
-hcg-help
  • Provided by: Heuristiccallgraph :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in heuristiccallgraph
-hcg-ignore-pointers
  • Provided by: Heuristiccallgraph
  • Type: boolean
  • Default: false
  • Opposite option: -hcg-no-ignore-pointers
  • ignore function pointers during computation of reachable functions
-hcg-ignore-pointers-print
  • Provided by: Heuristiccallgraph :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -hcg-no-ignore-pointers-print
  • print results for option -hcg-ignore-pointers
-hcg-msg-key
  • Provided by: Heuristiccallgraph :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -hcg-msg-key help to get a list of available categories, and * to enable all categories
-hcg-output
  • Provided by: Heuristiccallgraph
  • Type: string
  • Default: <none>
  • output the callgraph to a file; the output format is recognized through the extension.
-hcg-print
  • Provided by: Heuristiccallgraph :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -hcg-no-print
  • print results for option -hcg
-hcg-root
  • Provided by: Heuristiccallgraph
  • Type: set
  • Default: <none>
  • Categories: all
  • activate computation
-hcg-verbose
  • Provided by: Heuristiccallgraph :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in heuristiccallgraph
-impact-debug
  • Provided by: Impact :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in impact
-impact-graph
  • Provided by: Impact
  • Type: boolean
  • Default: false
  • Opposite option: -impact-no-graph
  • build a graph that explains why a statement is in the set of impacted nodes
-impact-help
  • Provided by: Impact :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in impact
-impact-in-callers
  • Provided by: Impact
  • Type: boolean
  • Default: true
  • Opposite option: -impact-not-in-callers
  • compute compute impact in callers as well as in callees
-impact-msg-key
  • Provided by: Impact :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -impact-msg-key help to get a list of available categories, and * to enable all categories
-impact-pragma
  • Provided by: Impact
  • Type: set
  • Default: <none>
  • Categories: all
  • use the impact pragmas in the code of functions f1,…,fn
-impact-print
  • Provided by: Impact
  • Type: boolean
  • Default: false
  • Opposite option: -impact-no-print
  • print the impacted stmt
-impact-skip
  • Provided by: Impact
  • Type: set
  • Default: <none>
  • Categories: <none>
  • consider that those variables are not impacted
-impact-slicing
  • Provided by: Impact
  • Type: boolean
  • Default: false
  • Opposite option: -impact-no-slicing
  • slice from the impacted stmt
-impact-verbose
  • Provided by: Impact :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in impact
-impactif
  • Provided by: Impactif
  • Type: boolean
  • Default: false
  • Opposite option: -no-impactif
  • Run the impactif analysis by interpreting the slicing pragma
-impactif-debug
  • Provided by: Impactif :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in impactif
-impactif-help
  • Provided by: Impactif :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in impactif
-impactif-msg-key
  • Provided by: Impactif :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -impactif-msg-key help to get a list of available categories, and * to enable all categories
-impactif-verbose
  • Provided by: Impactif :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in impactif
-implicit-function-declaration
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: warn
  • Possible values:error, ignore, warn
  • Warn or abort when a function is called before it has been declared (non-C99 compliant); action must be ignore, warn, or error
-info-compute
  • Provided by: Info :: Tuning
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-compute
  • do not output anything, but compute all the internal tables. This is useful for a saved project to save time later on when loading it.
-info-csv-all
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export all the computed information in csv files with filenames based on the specified basename
-info-csv-files
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about files in the specified csv file
-info-csv-functions
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about functions in the specified csv file
-info-csv-properties
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about properties in the specified csv file
-info-csv-shared-variables
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about shared variables in the specified csv file
-info-csv-statements
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about statements in the specified csv file
-info-csv-types
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about types in the specified csv file
-info-csv-variables
  • Provided by: Info :: CSV generation
  • Type: string
  • Default: <none>
  • export information about global variables in the specified csv file
-info-debug
  • Provided by: Info :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in info
-info-exit-status
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-exit-status
  • print information about the application exit status, and exit points. Needs value analysis results.
-info-files
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-files
  • print information about files from the current project.
-info-functions
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-functions
  • print information about functions from the current project.
-info-help
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in info
-info-help-files
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-files
  • print help about files information.
-info-help-functions
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-functions
  • print help about functions information.
-info-help-json-results
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-json-results
  • print help about the JSON format used in the file generated when using the ‘-info-json-results’ option.
-info-help-properties
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-properties
  • print help about properties information.
-info-help-reachable
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-reachable
  • print help about getting information about reachable statements.
-info-help-shared-variables
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-shared-variables
  • print help about getting information about shared variables.
-info-help-show
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-show
  • print more help about the ‘show’ queries.
-info-help-statements
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-statements
  • print help about getting information about statements.
-info-help-types
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-types
  • print help about getting information about types.
-info-help-variables
  • Provided by: Info :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-help-variables
  • print help about getting information about global variables.
-info-json-results
  • Provided by: Info :: Results
  • Type: string
  • Default: <none>
  • export the -info-results results to the given file using the JSON format.
-info-msg-key
  • Provided by: Info :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -info-msg-key help to get a list of available categories, and * to enable all categories
-info-precision
  • Provided by: Info
  • Type: integer
  • Default: 0
  • give information about loss of precision: 0 for none, 1 or more for more
-info-properties
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-properties
  • print information about properties from the current project.
-info-reachable
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-reachable
  • deprecated. Print messages about semantically reached statements.This is useful to collect information to compute the coverage on several analyses of the same functions.
-info-results
  • Provided by: Info :: Results
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-results
  • print an overview of the most important results of an analysis.
-info-results-skip-abort
  • Provided by: Info :: Results
  • Type: set
  • Default: <none>
  • Categories: <none>
  • specify a list of functions that are known to not terminate (such as ‘abort’ functions). They will be ignored in the -info-msg-key results:non-terminating output.
-info-results-skip-lib
  • Provided by: Info :: Results
  • Type: set
  • Default: <none>
  • Categories: <none>
  • specify a list of functions that are known to be library functions (i.e. with no body but a specification). They will be ignored in the -info-msg-key results:no-body-but-spec output.
-info-results-skip-log
  • Provided by: Info :: Results
  • Type: set
  • Default: <none>
  • Categories: <none>
  • specify a list of regular expressions that match messages to be considered as normal. The regular expressions are also compared to the plugin name to be able to ignore all the messages from a given plugin. They will be ignored in the -info-msg-key results:messages-terminating output.
-info-results-skip-props
  • Provided by: Info :: Results
  • Type: set
  • Default: <none>
  • Categories: <none>
  • specify a list of properties that can be ignored in the -info-msg-key results:hypotheses output because they are verified elsewhere. For instance, use ‘-info-results-skip-props _wp,_rv’ if the properties verified by WP have the ‘_wp’ suffix, and the properties manually reviewed have the ‘_rv’ suffix.
-info-shared-variables
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-shared-variables
  • print information about the shared variables after a Mthread analysis
-info-show-state
  • Provided by: Info :: Show queries
  • Type: list
  • Default: <none>
  • print the value of the computed state at the specified program point. The syntax to specify the program point is the same than for -info-show-val.
-info-show-statements
  • Provided by: Info :: Show queries
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-show-statements
  • print the selected statement for the queries that involve program points.
-info-show-val
  • Provided by: Info :: Show queries
  • Type: list
  • Default: <none>
  • print the value of the given term at the specified program point. More details about the syntax with the -info-help-show option.
-info-show-with-callstack
  • Provided by: Info :: Show queries
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-show-with-callstack
  • show the detailed values for each call stack.
-info-statements
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-statements
  • print information about statements
-info-stmt-no-reduction
  • Provided by: Info :: Tuning
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-stmt-no-reduction
  • in the ‘more’ column of the ‘test’ statements information, add ‘no reduction’ if the states are the same in both branches. Not enabled by default because its computation is expensive.
-info-types
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-types
  • print information about types
-info-variables
  • Provided by: Info
  • Type: boolean
  • Default: false
  • Opposite option: -info-no-variables
  • print information about global variables
-info-verbose
  • Provided by: Info :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in info
-info-with-stat
  • Provided by: Info :: Tuning
  • Type: boolean
  • Default: true
  • Opposite option: -info-without-stat
  • show the columns that hold the value analysis timing statistics in the results (default). It is useful to unset this option when the goal is to compare the results between several analyses because the timing may vary even when the other results remain the same.
-initialized-padding-locals
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-initialized-padding-locals
  • Implicit initialization of locals sets padding bits to 0. If false, padding bits are left uninitialized.
-inlining-mode
  • Provided by: Kernel :: Customizing Normalization
  • Type: string
  • Default: warn
  • Possible values:always, never, warn
  • Specify how to handle inline definitions: always use inline definitions, never use inline definitions, or never use inline definitions but emit a warning if they appear (this option does not concern static inline functions, extern inline functions, or functions with the “always_inline” attribute specified).
-inout
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-inout
  • Compute operational inputs, an over-approximation of the set of locations whose initial value is used; and the sure outputs, an under-approximation of the set of the certainly written locations
-inout-callwise
  • Provided by: Inout
  • Type: boolean
  • Default: true
  • Opposite option: -inout-no-callwise
  • Compute callsite-wise operational inputs using the joined states of the value analysis. This is faster and less precise than using the graph with -inout-callwise-on-graph.
-inout-callwise-on-graph
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -inout-no-callwise-on-graph
  • Compute callsite-wise operational inputs using the state graph computed by the value analysis.
-inout-debug
  • Provided by: Inout :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in inout
-inout-help
  • Provided by: Inout :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in inout
-inout-msg-key
  • Provided by: Inout :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -inout-msg-key help to get a list of available categories, and * to enable all categories
-inout-print
  • Provided by: Inout :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -inout-no-print
  • print the results of all the analyzes
-inout-verbose
  • Provided by: Inout :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in inout
-inout-with-formals
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -inout-no-with-formals
  • same as -inout but without local variables and with function parameters
-input
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-input
  • Compute imperative inputs. Locals and function parameters are not displayed
-input-with-formals
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-input-with-formals
  • Compute imperative inputs. Function parameters are displayed, locals are not
-integer-constants
  • Provided by: Kernel :: Customizing Normalization
  • Type: string
  • Default: c99strict
  • Possible values:c89clang, c89strict, c99clang, c99strict
  • Use one of c99strict, c89strict, c99clang, c89clang as choice for typing integer constants
-java-check-mode
  • Provided by: Java
  • Type: string
  • Default: ignore
  • Possible values:compliant, ignore, strict
  • changes the way check instructions are translated; ignore does not translate checks; strict translates checks using the tis_ub builtin; and compliant translates checks by using the Java/JVM specification to raise the correct exception.
-java-class
  • Provided by: Java
  • Type: set
  • Default: <none>
  • Categories: <none>
  • Add class to list of translated classes
-java-debug
  • Provided by: Java :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Java
-java-debug-fir
  • Provided by: Java
  • Type: string
  • Default: nnnnnn
  • abcdef where: a is before odr cache optimization; b is before class declaration completion; c is before lift; d is before reorder; e is before class definition completion; and f is the final result.
-java-frontend
  • Provided by: Java
  • Type: string
  • Default: tis-javafrontend
  • use <cmd> as the parsing command.
-java-help
  • Provided by: Java :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Java
-java-keep-synchronized
  • Provided by: Java
  • Type: boolean
  • Default: false
  • Opposite option: -java-no-keep-synchronized
  • keep the synchronization while translating synchronized blocks or methods.
-java-msg-key
  • Provided by: Java :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -java-msg-key help to get a list of available categories, and * to enable all categories
-java-runtime
  • Provided by: Java
  • Type: boolean
  • Default: false
  • Opposite option: -no-java-runtime
  • Adds runtime files for the Java plugin.
-java-verbose
  • Provided by: Java :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Java
-jessie3-debug
  • Provided by: Jessie3 :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Jessie3
-jessie3-help
  • Provided by: Jessie3 :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Jessie3
-jessie3-msg-key
  • Provided by: Jessie3 :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -jessie3-msg-key help to get a list of available categories, and * to enable all categories
-jessie3-share
  • Provided by: Jessie3
  • Type: string
  • Default: <none>
  • set the plug-in share directory to <dir> (may be used if the plug-in is not installed at the same place as TrustInSoft Kernel)
-jessie3-verbose
  • Provided by: Jessie3 :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Jessie3
-keep-comments
  • Provided by: Kernel :: Input/Output Source Code
  • Type: boolean
  • Default: false
  • Opposite option: -no-keep-comments
  • try to keep comments in C code
-keep-switch
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-keep-switch
  • keep switch statements despite -simplify-cfg
-keep-unused-specified-functions
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -remove-unused-specified-functions
  • keep specified-but-unused functions
-keep-unused-static-functions
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -remove-unused-static-functions
  • keep unused static functions
-kernel-debug
  • Provided by: Kernel :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for the TrustInSoft Kernel
-kernel-help
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of the TrustInSoft Kernel
-kernel-msg-key
  • Provided by: Kernel :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -kernel-msg-key help to get a list of available categories, and * to enable all categories
-kernel-verbose
  • Provided by: Kernel :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for the TrustInSoft Kernel
-label-annotations-by-emitter
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-label-annotations-by-emitter
  • Automatically add the label p: to annotations emitted by the plug-in p
-language
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: unspecified
  • Possible values:c, c++, java, unspecified
  • process input file(s) as the given language regardless of the file extension. Allowed values are “unspecified”, “c” and “c++”.
-language-mode
  • Provided by: Mode
  • Type: string
  • Default: c
  • Possible values:c, c++, cxx
  • Define the language mode to use, hence update a set of other command line options to properly analyze a program in the given language.
-lib-entry
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-lib-entry
  • run analysis for an incomplete application e.g. an API call. See the -main option to set the entry point
-load
  • Provided by: Kernel :: Saving or Loading Data
  • Type: string
  • Default: <none>
  • load a previously-saved session from file <filename>
-load-and-dump
  • Provided by: Kernel :: Saving or Loading Data
  • Type: string
  • Default: <none>
  • like -load but also dumps the state sizes for each project in <filename>_<n>.size
-load-module
  • Provided by: Kernel :: Saving or Loading Data
  • Type: list
  • Default: tests/help/options.ml
  • Dynamically load plug-ins, modules and scripts. Each <SPEC> can be an OCaml source or object file, with or without extension, or a directory of object OCaml files to load, or a Findlib package. Loading order is preserved and additional dependencies can be listed in *.depend files.
-machdep
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: gcc_x86_32
  • use <machine> as the current machine dependent configuration. See “-machdep help” for a list and “-machdep verbose” for a brief summary of the main characteristics of each.
-main
  • Provided by: Kernel :: Analysis Options
  • Type: string
  • Default: main
  • use <f> as entry point for analysis. See “-lib-entry” if this is not for a complete application.
-memexec-all
  • Provided by: Value analysis :: Precision vs. time
  • Type: boolean
  • Default: false
  • Opposite option: -no-memexec-all
  • (experimental) speed up analysis by not recomputing functions already analyzed in the same context. Incompatible with some plugins and callbacks
-memory-region
  • Provided by: Kernel :: Analysis Options
  • Type: map
  • Default: <none>
  • Categories: <none>
  • give names to memory regions. The only purpose of those names is that they can be used as shortcuts in address specifications (in -absolute-address for instance). A region may be defined by an address range ‘[<min>..<max>]’ or a base address and a size ‘<base>[<size>]’ which is equivalent to ‘[<base>..<base>+<size>-1]’.
-merging-strategy
  • Provided by: Kernel :: Customizing Normalization
  • Type: string
  • Default: all-together
  • Possible values:all-together, fold-left, individual-then-all-together
  • Specify how to merge the input files: merge them all together simultaneously (default), or merge by left-folding (i.e. merge two first files, then merge the result with the third file, and so on), or “merge” each file individually (put each file separately through the merging process, just to check if this does not alter its semantics) and then merge the results for all the files together. Ideally the merging strategy should not change the behavior of the merged program, but some quirks are possible (especially in merging-related features like weak definitions, where the order matters). This feature is experimental and meant exclusively for development and testing!
-metrics
  • Provided by: Metrics
  • Type: boolean
  • Default: false
  • Opposite option: -no-metrics
  • activate metrics computation
-metrics-ast
  • Provided by: Metrics
  • Type: string
  • Default: cil
  • Possible values:acsl, cabs, cil
  • apply metrics to Cabs or CIL AST, or to ACSL specs
-metrics-by-function
  • Provided by: Metrics
  • Type: boolean
  • Default: false
  • Opposite option: -metrics-no-by-function
  • also compute metrics on a per-function basis
-metrics-by-function-print
  • Provided by: Metrics :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -metrics-no-by-function-print
  • print results for option -metrics-by-function
-metrics-cover
  • Provided by: Metrics
  • Type: set
  • Default: <none>
  • Categories: all
  • compute an overapproximation of the functions reachable from f1,..,fn.
-metrics-debug
  • Provided by: Metrics :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in metrics
-metrics-help
  • Provided by: Metrics :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in metrics
-metrics-libc
  • Provided by: Metrics
  • Type: boolean
  • Default: false
  • Opposite option: -metrics-no-libc
  • show functions from TrustInSoft Kernel standard C library in the results; deactivated by default.
-metrics-msg-key
  • Provided by: Metrics :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -metrics-msg-key help to get a list of available categories, and * to enable all categories
-metrics-output
  • Provided by: Metrics
  • Type: string
  • Default: <none>
  • print some metrics into the specified file; the output format is recognized by its extension (html or txt).
-metrics-print
  • Provided by: Metrics :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -metrics-no-print
  • print results for option -metrics
-metrics-value-cover
  • Provided by: Metrics
  • Type: boolean
  • Default: false
  • Opposite option: -metrics-no-value-cover
  • estimate value analysis coverage w.r.t. to reachable syntactic definitions
-metrics-value-cover-print
  • Provided by: Metrics :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -metrics-no-value-cover-print
  • print results for option -metrics-value-cover
-metrics-verbose
  • Provided by: Metrics :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in metrics
-mode-debug
  • Provided by: Mode :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Mode
-mode-help
  • Provided by: Mode :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Mode
-mode-msg-key
  • Provided by: Mode :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -mode-msg-key help to get a list of available categories, and * to enable all categories
-mode-verbose
  • Provided by: Mode :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Mode
-mt-compact
  • Provided by: Mthread :: Multithreaded control-flow-graph
  • Type: set
  • Default: <none>
  • Categories: <none>
  • do not show the body of the given functions
-mt-debug
  • Provided by: Mthread :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in mthread
-mt-extract
  • Provided by: Mthread :: Extraction of models
  • Type: set
  • Default: <none>
  • Categories: <none>
  • extraction of models
-mt-full-cfg
  • Provided by: Mthread :: Multithreaded control-flow-graph
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-full-cfg
  • Do not simplify cfg and show all statements (can be costly)
-mt-help
  • Provided by: Mthread :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in mthread
-mt-ignore-null
  • Provided by: Mthread :: Debug
  • Type: boolean
  • Default: false
  • Opposite option: -mt-consider-null
  • Ignore shared accesses to numeric memory (NULL base)
-mt-inline-callbacks
  • Provided by: Mthread :: Multithreaded control-flow-graph
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-inline-callbacks
  • Do not show the names of concurrent primitives, only their effect
-mt-keep-all-analyses
  • Provided by: Mthread :: Debug
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-keep-all-analyses
  • Keep a copy of all the analyses done for each thread
-mt-keep-dot
  • Provided by: Mthread :: Debug
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-keep-dot
  • keep dot files generated by the html output
-mt-moderate-warnings
  • Provided by: Mthread :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -mt-no-moderate-warnings
  • Show semi-important warnings during analysis.
-mt-msg-key
  • Provided by: Mthread :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -mt-msg-key help to get a list of available categories, and * to enable all categories
-mt-nice-offsets
  • Provided by: Mthread :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -mt-no-nice-offsets
  • Try to display nice offsets for objects names
-mt-non-concurrent-accesses
  • Provided by: Mthread :: Multithreaded control-flow-graph
  • Type: boolean
  • Default: true
  • Opposite option: -mt-no-non-concurrent-accesses
  • Keep non-concurrent accesses to shared variables in the cfg
-mt-non-shared-accesses
  • Provided by: Mthread :: Multithreaded control-flow-graph
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-non-shared-accesses
  • Keep accesses to false shared variables in the cfg
-mt-only-threads
  • Provided by: Mthread :: Debug
  • Type: set
  • Default: <none>
  • Categories: <none>
  • only execute the specified threads
-mt-print-callstacks
  • Provided by: Mthread :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-print-callstacks
  • Print the callstacks at which concurrent events occur
-mt-projects-on-disk
  • Provided by: Mthread :: Debug
  • Type: boolean
  • Default: false
  • Opposite option: -mt-projects-together
  • Save the copies of the analyses in a separate file, instead of all together
-mt-projects-on-disk-prefix
  • Provided by: Mthread :: Debug
  • Type: string
  • Default: th
  • Prepend <prefix> to the project’s filename saved by -mt-projects-on-disk (defaults to th)
-mt-return-edges
  • Provided by: Mthread :: Multithreaded control-flow-graph
  • Type: boolean
  • Default: true
  • Opposite option: -mt-no-return-edges
  • Show link between a call an a return instruction as a dotted line
-mt-share
  • Provided by: Mthread
  • Type: string
  • Default: <none>
  • set the plug-in share directory to <dir> (may be used if the plug-in is not installed at the same place as TrustInSoft Kernel)
-mt-shared-accesses-synchronization
  • Provided by: Mthread :: Analysis
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-shared-accesses-synchronization
  • more precise inference of which mutexes protect shared memory
-mt-shared-values
  • Provided by: Mthread :: Analysis
  • Type: integer
  • Default: 0
  • Possible values: between 0 and 2
  • Show what threads read and write in shared memory at the end of each iteration 0: values not shown 1: values shown 2: values shown with the stack at which the operation occurs
-mt-show-sids
  • Provided by: Mthread :: Debug
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-show-sids
  • Show statement ids when printing line numbers
-mt-skip-threads
  • Provided by: Mthread :: Debug
  • Type: set
  • Default: <none>
  • Categories: <none>
  • do not execute the specified threads
-mt-stop-after
  • Provided by: Mthread :: Debug
  • Type: integer
  • Default: 4611686018427387903
  • Only perform at most i iterations
-mt-time
  • Provided by: Mthread :: Debug
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-time
  • Show time taken by thread computation
-mt-use-slevel
  • Provided by: Mthread :: Analysis
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-use-slevel
  • use slevel information coming from Value. Option -val-slevel-results must also be set
-mt-verbose
  • Provided by: Mthread :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in mthread
-mt-write-races
  • Provided by: Mthread :: Analysis
  • Type: boolean
  • Default: false
  • Opposite option: -mt-no-write-races
  • Display memory on which there is a write-only race condition
-mthread
  • Provided by: Mthread
  • Type: boolean
  • Default: false
  • Opposite option: -no-mthread
  • enable analysis of multi-threaded programs through the Mthread plugin
-no-fs
  • Provided by: Tis-mkfs
  • Type: boolean
  • Default: false
  • Opposite option: -empty-fs
  • Do not use any filesystem model (see -fs option). Beware: this may lead to imprecise results when analyzing functions related with filesystem operations. Automatically set when -no-tis-libc is set.
-no-results
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: false
  • Opposite option: -val-store-results
  • do not record values for any of the statements of the program
-no-results-function
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: set
  • Default: <none>
  • Categories: all
  • do not record the values obtained for the statements of function f
-noreturn
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: c11
  • indicates whether the C11 function specifier “_Noreturn” is recognized.
-obfuscate
  • Provided by: Obfuscator
  • Type: boolean
  • Default: false
  • Opposite option: -no-obfuscate
  • print an obfuscated version of the input files and exit. Disable any other TrustInSoft Kernel analysis.
-obfuscator-debug
  • Provided by: Obfuscator :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in obfuscator
-obfuscator-dictionary
  • Provided by: Obfuscator
  • Type: string
  • Default: <none>
  • generate the dictionary into file <f> (on stdout by default)
-obfuscator-help
  • Provided by: Obfuscator :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in obfuscator
-obfuscator-msg-key
  • Provided by: Obfuscator :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -obfuscator-msg-key help to get a list of available categories, and * to enable all categories
-obfuscator-string-dictionary
  • Provided by: Obfuscator
  • Type: string
  • Default: <none>
  • generate the dictionary of literal strings into file <f> (in the same place than the code by default)
-obfuscator-verbose
  • Provided by: Obfuscator :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in obfuscator
-obviously-terminates
  • Provided by: Value analysis :: Deterministic programs
  • Type: boolean
  • Default: false
  • Opposite option: -no-obviously-terminates
  • undocumented. Among effects of this options are the same effects as -no-results and -no-inclusion-check
-obviously-terminates-function
  • Provided by: Value analysis :: Deterministic programs
  • Type: set
  • Default: <none>
  • Categories: all
-occurrence
  • Provided by: Occurrence
  • Type: boolean
  • Default: false
  • Opposite option: -no-occurrence
  • print results of occurrence analysis
-occurrence-debug
  • Provided by: Occurrence :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in occurrence
-occurrence-help
  • Provided by: Occurrence :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in occurrence
-occurrence-msg-key
  • Provided by: Occurrence :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -occurrence-msg-key help to get a list of available categories, and * to enable all categories
-occurrence-verbose
  • Provided by: Occurrence :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in occurrence
-ocode
  • Provided by: Kernel :: Input/Output Source Code
  • Type: string
  • Default: <none>
  • when printing code, redirects the output to file <filename>
-old-slevel-counter
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-old-slevel-counter
  • Disable the recent change on slevel counter
-orig-name
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: false
  • Opposite option: -no-orig-name
  • prints a message each time a variable is renamed
-out
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-out
  • Compute internal out. Those are an over-approximation of the set of written locations
-out-external
  • Provided by: Inout
  • Type: boolean
  • Default: false
  • Opposite option: -no-out-external
  • Compute external out. Those are an over-approximation of the set of written locations, excluding locals
-pdg
  • Provided by: Pdg
  • Type: boolean
  • Default: false
  • Opposite option: -no-pdg
  • build the dependence graph of each function
-pdg-debug
  • Provided by: Pdg :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in pdg
-pdg-dot
  • Provided by: Pdg :: Output
  • Type: string
  • Default: <none>
  • put the PDG of function <f> in basename.f.dot
-pdg-help
  • Provided by: Pdg :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in pdg
-pdg-msg-key
  • Provided by: Pdg :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -pdg-msg-key help to get a list of available categories, and * to enable all categories
-pdg-print
  • Provided by: Pdg :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -pdg-no-print
  • print results for option -pdg
-pdg-verbose
  • Provided by: Pdg :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in pdg
-permissive
  • Provided by: Kernel :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-permissive
  • performs less verification on validity of command-line options
-plevel
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 200
  • Possible values: between 1 and 1000000000
  • use <n> as the precision level for arrays accesses. Array accesses are precise as long as the interval for the index contains less than n values.
-pointer-arguments-to-std-functions
  • Provided by: Kernel :: Analysis Options
  • Type: string
  • Default: strict
  • Possible values:loose, nonnull, strict
  • set the kinds of enforcement for the validity of arguments to standard library functions like memcmp. Allowed values are “strict”, “nonnull” and “loose”.
-postdominators-debug
  • Provided by: Postdominators :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in postdominators
-postdominators-help
  • Provided by: Postdominators :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in postdominators
-postdominators-msg-key
  • Provided by: Postdominators :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -postdominators-msg-key help to get a list of available categories, and * to enable all categories
-postdominators-verbose
  • Provided by: Postdominators :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in postdominators
-pp-annot
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: <none>
  • Opposite option: -no-pp-annot
  • pre-process annotations (if they are read). Set by default if the pre-processor is GNU-like (see option -cpp-gnu-like)
-pre-file
  • Provided by: Kernel
  • Type: list
  • Default: <none>
  • Add the given file to be parsed before any other files, including runtime files automatically added by TIS-Kernel.
-print
  • Provided by: Kernel :: Input/Output Source Code
  • Type: boolean
  • Default: false
  • Opposite option: -no-print
  • pretty print original code with its comments
-print-config
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • print full config information
-print-lib-path
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • print the path of the TrustInSoft Kernel library
-print-pid
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: -no-print-pid
  • print the pid of the main process. Set by default unless the TIS_KERNEL_TEST_MODE environment variable is set to some non-empty value.
-print-plugin-path
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • print the path where the TrustInSoft Kernel dynamic plug-ins are searched into
-print-share-path
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • print the TrustInSoft Kernel share path
-print-version
  • Provided by: Kernel :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • print the TrustInSoft Kernel version
-print_api
  • Provided by: Print interface
  • Type: string
  • Default: <none>
  • creates a .mli file for the dynamic plugins inside the supplied directory
-print_api-debug
  • Provided by: Print interface :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Print interface
-print_api-help
  • Provided by: Print interface :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Print interface
-print_api-msg-key
  • Provided by: Print interface :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -print_api-msg-key help to get a list of available categories, and * to enable all categories
-print_api-verbose
  • Provided by: Print interface :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Print interface
-quiet
  • Provided by: Kernel :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • sets -verbose and -debug to 0
-remove-exn
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-remove-exn
  • transforms throw and try/catch statements to normal C functions. Disabled by default, unless input source language has has an exception mechanism.
-remove-projects
  • Provided by: Kernel :: Project-related Options
  • Type: set
  • Default: <none>
  • Categories: all, all\_but\_current
  • remove the given projects <p1>, …, <pn>. @all_but_current removes all projects but the current one.
-remove-redundant-alarms
  • Provided by: Value analysis :: Precision vs. time
  • Type: boolean
  • Default: true
  • Opposite option: -no-remove-redundant-alarms
  • after the analysis, try to remove redundant alarms, so that the user needs inspect fewer of them
-remove-volatile-locals
  • Provided by: Kernel :: Customizing Normalization
  • Type: set
  • Default: <none>
  • Categories: <none>
  • remove the qualifier “volatile” from all local variables of given set of functions
-report
  • Provided by: Report
  • Type: boolean
  • Default: false
  • Opposite option: -no-report
  • display a summary of properties status
-report-csv
  • Provided by: Report
  • Type: string
  • Default: <none>
  • if set, output properties as a csv file of the given name
-report-debug
  • Provided by: Report :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in report
-report-help
  • Provided by: Report :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in report
-report-msg-key
  • Provided by: Report :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -report-msg-key help to get a list of available categories, and * to enable all categories
-report-print-properties
  • Provided by: Report
  • Type: boolean
  • Default: false
  • Opposite option: -report-no-print-properties
  • print not only the locations, but also the properties themselves
-report-proven
  • Provided by: Report
  • Type: boolean
  • Default: true
  • Opposite option: -report-no-proven
  • if set, output proven properties. Otherwise, only unproven ones are shown.
-report-specialized
  • Provided by: Report
  • Type: boolean
  • Default: true
  • Opposite option: -report-no-specialized
  • display properties that are auxiliary instances of other properties.
-report-untried
  • Provided by: Report
  • Type: boolean
  • Default: false
  • Opposite option: -report-no-untried
  • display properties which no plug-in tried to prove
-report-verbose
  • Provided by: Report :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in report
-resume-value
  • Provided by: Resume
  • Type: boolean
  • Default: false
  • Opposite option: -no-resume-value
  • Resume aborted analyses of Value
-rm-unused-globals
  • Provided by: Sparecode
  • Type: boolean
  • Default: false
  • Opposite option: -no-rm-unused-globals
  • only remove unused global types and variables (automatically done by -sparecode-analysis)
-rte
  • Provided by: Rtegen
  • Type: boolean
  • Default: false
  • Opposite option: -no-rte
  • generates annotations for runtime error checking and preconditions at call sites
-rte-all
  • Provided by: Rtegen
  • Type: boolean
  • Default: true
  • Opposite option: -rte-no-all
  • generate everything (supersedes all -rte-no-*)
-rte-debug
  • Provided by: Rtegen :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in rtegen
-rte-div
  • Provided by: Rtegen
  • Type: boolean
  • Default: true
  • Opposite option: -rte-no-div
  • annotate for modulo and division by zero
-rte-float-to-int
  • Provided by: Rtegen
  • Type: boolean
  • Default: true
  • Opposite option: -rte-no-float-to-int
  • annotate casts from floating-point to integer
-rte-help
  • Provided by: Rtegen :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in rtegen
-rte-mem
  • Provided by: Rtegen
  • Type: boolean
  • Default: true
  • Opposite option: -rte-no-mem
  • annotate for valid pointer or array access
-rte-msg-key
  • Provided by: Rtegen :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -rte-msg-key help to get a list of available categories, and * to enable all categories
-rte-precond
  • Provided by: Rtegen
  • Type: boolean
  • Default: false
  • Opposite option: -rte-no-precond
  • generate assertions on function calls based on contracts
-rte-select
  • Provided by: Rtegen
  • Type: set
  • Default: <none>
  • Categories: all
  • select <fun> for analysis
-rte-shift
  • Provided by: Rtegen
  • Type: boolean
  • Default: true
  • Opposite option: -rte-no-shift
  • annotate for left and right shifts by a value out of bounds
-rte-trivial-annotations
  • Provided by: Rtegen
  • Type: boolean
  • Default: false
  • Opposite option: -rte-no-trivial-annotations
  • generate annotations for constant expressions, even when they trivially hold
-rte-verbose
  • Provided by: Rtegen :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in rtegen
-rte-warn
  • Provided by: Rtegen
  • Type: boolean
  • Default: true
  • Opposite option: -rte-no-warn
  • emits warning on broken asserts
-sa
  • Provided by: Strict aliasing
  • Type: boolean
  • Default: false
  • Opposite option: -no-sa
  • Activate the analysis to detect strict aliasing violation.
-sa-debug
  • Provided by: Strict aliasing :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in strict aliasing
-sa-help
  • Provided by: Strict aliasing :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in strict aliasing
-sa-msg-key
  • Provided by: Strict aliasing :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -sa-msg-key help to get a list of available categories, and * to enable all categories
-sa-strict-enum
  • Provided by: Strict aliasing
  • Type: boolean
  • Default: false
  • Opposite option: -sa-no-strict-enum
  • Consider enum types as enumeration, not as their integer representation. Access to an enum cell requires the same enum type and not the same integer representation.
-sa-strict-struct
  • Provided by: Strict aliasing
  • Type: boolean
  • Default: false
  • Opposite option: -sa-no-strict-struct
  • Access to an object marked by a structure effective type has to be made throught the exact same structure type.
-sa-strict-union
  • Provided by: Strict aliasing
  • Type: boolean
  • Default: true
  • Opposite option: -sa-no-strict-union
  • Access to an object marked by an union effective type has to be made through the exact same union type.
-sa-verbose
  • Provided by: Strict aliasing :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in strict aliasing
-safe-arrays
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: true
  • Opposite option: -unsafe-arrays
  • for multidimensional arrays or arrays that are fields inside structs, assume that accesses are in bounds
-save
  • Provided by: Kernel :: Saving or Loading Data
  • Type: string
  • Default: <none>
  • at exit, save the session into file <filename>
-scf
  • Provided by: Semantic constant folding
  • Type: boolean
  • Default: false
  • Opposite option: -no-scf
  • pretty print a version of the source code where each constant expression is replaced by its value
-scf-allow-cast
  • Provided by: Semantic constant folding
  • Type: boolean
  • Default: false
  • Opposite option: -scf-no-allow-cast
  • replace expressions by constants even when doing so requires a pointer cast
-scf-debug
  • Provided by: Semantic constant folding :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in semantic constant folding
-scf-fct
  • Provided by: Semantic constant folding
  • Type: set
  • Default: <none>
  • Categories: all
  • propagate constants only into functions f1,…,fn
-scf-help
  • Provided by: Semantic constant folding :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in semantic constant folding
-scf-logic
  • Provided by: Semantic constant folding
  • Type: boolean
  • Default: false
  • Opposite option: -scf-no-logic
  • replace values from logical context and create corresponding variables (HIGHLY EXPERIMENTAL)
-scf-msg-key
  • Provided by: Semantic constant folding :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -scf-msg-key help to get a list of available categories, and * to enable all categories
-scf-project-name
  • Provided by: Semantic constant folding
  • Type: string
  • Default: propagated
  • name of the generated project
-scf-verbose
  • Provided by: Semantic constant folding :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in semantic constant folding
-scope-debug
  • Provided by: Scope :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in scope
-scope-defs-interproc
  • Provided by: Scope
  • Type: boolean
  • Default: true
  • Opposite option: -scope-no-defs-interproc
  • interprocedural defs computation
-scope-help
  • Provided by: Scope :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in scope
-scope-msg-key
  • Provided by: Scope :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -scope-msg-key help to get a list of available categories, and * to enable all categories
-scope-verbose
  • Provided by: Scope :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in scope
-separate-n
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 0
  • Possible values: between 0 and 1073741823
-separate-of
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 0
  • Possible values: between 0 and 1073741823
-separate-stmts
  • Provided by: Value analysis :: Precision vs. time
  • Type: set
  • Default: <none>
  • Categories: <none>
-server
  • Provided by: Server :: Web Server Configuration
  • Type: boolean
  • Default: false
  • Opposite option: -no-server
  • Start the GUI so it becomes available from a web browser
-server-cpp
  • Provided by: Server
  • Type: boolean
  • Default: false
  • Opposite option: -server-no-cpp
  • enable the C++ mode for the server
-server-debug
  • Provided by: Server :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Server
-server-expose
  • Provided by: Server :: Web Server Configuration
  • Type: boolean
  • Default: false
  • Opposite option: -server-no-expose
  • When set, the GUI will accept connections from anywhere. Otherwise, only a browser running on the same computer as TrustInSoft Analyzer may access the GUI.
-server-help
  • Provided by: Server :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Server
-server-msg-key
  • Provided by: Server :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -server-msg-key help to get a list of available categories, and * to enable all categories
-server-name
  • Provided by: Server :: Web Server Configuration
  • Type: string
  • Default: <none>
  • Choose a name for this TrustInSoft Analyzer instance. The name is displayed in the GUI, allowing to identify more easily this instance when several instances of TrustInSoft Analyzer are running at the same time. The default name is the entry point of the program.
-server-port
  • Provided by: Server :: Web Server Configuration
  • Type: integer
  • Default: 8080
  • Choose a specific port for the GUI to listen to
-server-port-auto
  • Provided by: Server :: Web Server Configuration
  • Type: boolean
  • Default: false
  • Opposite option: -server-no-port-auto
  • Automatically choose a free unprivileged port (between 5000 and 20000). If this option is active, then the option -server-port is ignored
-server-verbose
  • Provided by: Server :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Server
-session
  • Provided by: Kernel :: Saving or Loading Data
  • Type: string
  • Default: <none>
  • directory in which session files are searched
-set-project-as-default
  • Provided by: Kernel :: Project-related Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-set-project-as-default
  • the current project becomes the default one (and so future ‘-then’ sequences are applied on it)
-show-indirect-deps
  • Provided by: From analysis
  • Type: boolean
  • Default: true
  • Opposite option: -no-show-indirect-deps
  • experimental
-simplify-cfg
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-simplify-cfg
  • remove break, continue and switch statements before analyses
-simplify-trivial-loops
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: true
  • Opposite option: -no-simplify-trivial-loops
  • simplify trivial loops, such as do … while(0) loops
-slevel
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 0
  • Possible values: between -1 and 1073741823
  • superpose up to <n> states when unrolling control flow. The larger n, the more precise and expensive the analysis.
-slevel-function
  • Provided by: Value analysis :: Precision vs. time
  • Type: map
  • Default: <none>
  • Categories: <none>
  • override slevel with <n> when analyzing <f>
-slice-assert
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • select the assertions of functions f1,…,fn
-slice-callers
  • Provided by: Slicing
  • Type: boolean
  • Default: true
  • Opposite option: -no-slice-callers
  • propagate the slicing to the function callers
-slice-calls
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • select every calls to functions f1,…,fn, and all their effect
-slice-force
  • Provided by: Slicing
  • Type: boolean
  • Default: true
  • Opposite option: -no-slice-force
  • force slicing
-slice-loop-inv
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • select the loop invariants of functions f1,…,fn
-slice-loop-var
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • select the loop variants of functions f1,…,fn
-slice-pragma
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • use the slicing pragmas in the code of functions f1,…,fn as slicing criteria: //@ slice pragma ctrl; to reach this control-flow point //@ slice pragma expr <expr_desc;>to preserve the value of an expression at this control-flow point //@ slice pragma stmt; to preserve the effect of the next statement
-slice-rd
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: <none>
  • select the read accesses to left-values v1,…,vn (addresses are evaluated at the beginning of the function given as entry point)
-slice-return
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • select the result (returned value) of functions f1,…,fn
-slice-threat
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: all
  • select the threats of functions f1,…,fn
-slice-undef-functions
  • Provided by: Slicing
  • Type: boolean
  • Default: false
  • Opposite option: -no-slice-undef-functions
  • allow the use of the -slicing-level option for calls to undefined functions
-slice-value
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: <none>
  • select the result of left-values v1,…,vn at the end of the function given as entry point (addresses are evaluated at the beginning of the function given as entry point)
-slice-wr
  • Provided by: Slicing
  • Type: set
  • Default: <none>
  • Categories: <none>
  • select the write accesses to left-values v1,…,vn (addresses are evaluated at the beginning of the function given asentry point)
-slicing-debug
  • Provided by: Slicing :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in slicing
-slicing-exported-project-postfix
  • Provided by: Slicing
  • Type: string
  • Default: export
  • postfix added to the slicing project name for building the name of the exported project (defaults to ” export”)
-slicing-help
  • Provided by: Slicing :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in slicing
-slicing-keep-annotations
  • Provided by: Slicing
  • Type: boolean
  • Default: false
  • Opposite option: -slicing-no-keep-annotations
  • keep annotations as long as the used variables are declared and the accessibility of the program point is preserved (even if the value of the data is not preserved)
-slicing-level
  • Provided by: Slicing
  • Type: integer
  • Default: 2
  • Possible values: between 0 and 3
  • set the default level of slicing used to propagate to the calls 0 : don’t slice the called functions 1 : don’t slice the called functions but propagate the marks anyway 2 : try to use existing slices, create at most one 3 : most precise slices note: this value (defaults to 2) is not used for calls to undefined functions except when ‘-slice-undef-functions’ option is set
-slicing-msg-key
  • Provided by: Slicing :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -slicing-msg-key help to get a list of available categories, and * to enable all categories
-slicing-project-name
  • Provided by: Slicing
  • Type: string
  • Default: Slicing
  • name of the slicing project (defaults to “Slicing”).This name is used as basename when building the name of the exported project (see -slicing-exported-project-postfix option)
-slicing-verbose
  • Provided by: Slicing :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in slicing
-sparecode
  • Provided by: Sparecode
  • Type: boolean
  • Default: false
  • Opposite option: -no-sparecode
  • perform a spare code analysis
-sparecode-annot
  • Provided by: Sparecode
  • Type: boolean
  • Default: true
  • Opposite option: -sparecode-no-annot
  • select more things to keep every reachable annotation
-sparecode-debug
  • Provided by: Sparecode :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in sparecode
-sparecode-help
  • Provided by: Sparecode :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in sparecode
-sparecode-msg-key
  • Provided by: Sparecode :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -sparecode-msg-key help to get a list of available categories, and * to enable all categories
-sparecode-verbose
  • Provided by: Sparecode :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in sparecode
-strict-type-qualifier-merging
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-strict-type-qualifier-merging
  • Strictly enforce type compatibility rules with respect to type qualifiers.
-time
  • Provided by: Kernel :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -no-time
  • Enable the time recording and performance measurements of the analyzer.
-time-flamegraph
  • Provided by: Kernel :: Output Messages
  • Type: string
  • Default: <none>
  • Output the whole performance summary given to the given filename as a Flame Graph (see also http://www.brendangregg.com/flamegraphs.html). All available details are dumped in the graph regardless of the verbosity given to the option “-time-verbose”. Implies option “-time”. Does not conflict with option “-time-output”.
-time-output
  • Provided by: Kernel :: Output Messages
  • Type: string
  • Default: <none>
  • Output the performance summary to the given filename. The summary details also depends on the verbosity given to the option “-time-verbose”. Implies option “-time”.
-time-verbose
  • Provided by: Kernel :: Output Messages
  • Type: integer
  • Default: 0
  • Set the verbosity of the “-time” option. <0> disables any message except the final summary. <1> enables messages when a major time category begins or stops to be recorded. <2> and over increases the details given in the final summary.
-tis-config-load
  • Provided by: Kernel :: Configuration files
  • Type: string
  • Default: <none>
  • Load the given configuration file. Learn more about configuration files in the documentation in the ‘Reference Manual > Configuration files’ section.
-tis-config-save
  • Provided by: Kernel :: Configuration files
  • Type: string
  • Default: <none>
  • If given, the current state (limited to the options supported in the configuration files) of the analyzer is saved into the given configuration file right before the analyzer exits.
-tis-config-select
  • Provided by: Kernel :: Configuration files
  • Type: integer
  • Default: <none>
  • If the configuration file loaded by ‘-tis-config-load’ contains several analysis configurations, the <n>th analysis configuration will be selected as the default one. The default analysis configuration is the first one. The <n> parameter must be a strictly positive integer. Exits with an error if <n> is greater than the number of analysis configurations in the file. This option is incompatible with the -tis-config-select-by-name one.
-tis-config-select-by-name
  • Provided by: Kernel :: Configuration files
  • Type: string
  • Default: <none>
  • If the configuration file loaded by ‘-tis-config-load’ contains several analysis configurations, the analysis configuration matching the given name will be selected as the default one. The default analysis configuration is the first one. Exits with an error if the given name does not match any analysis configuration in the file. This option is incompatible with the -tis-config-select one.
-tis-degenerate-or-inject
  • Provided by: Value analysis
  • Type: integer
  • Default: <none>
  • force tis_degenerate_or_inject to return <n>
-tis-interpreter-libc
  • Provided by: Value analysis :: Deterministic programs
  • Type: boolean
  • Default: false
  • Opposite option: -no-tis-interpreter-libc
  • Use the tis-interpreter default libc.
-tis-kernel-stdlib
  • Provided by: Kernel :: Parsing
  • Type: boolean
  • Default: false
  • Opposite option: -no-tis-kernel-stdlib
  • adds -I$TIS_KERNEL_SHARE/libc to the options given to the cpp command. If -cpp-gnu-like is not false, also adds -nostdinc to prevent inconsistent mix of system and TrustInSoft Kernel header files
-tis-libc
  • Provided by: Tis-Utils
  • Type: boolean
  • Default: true
  • Opposite option: -no-tis-libc
  • Use TrustInSoft Analyzer default libc.
-tis-mkfs-debug
  • Provided by: Tis-mkfs :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in tis-mkfs
-tis-mkfs-help
  • Provided by: Tis-mkfs :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in tis-mkfs
-tis-mkfs-msg-key
  • Provided by: Tis-mkfs :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -tis-mkfs-msg-key help to get a list of available categories, and * to enable all categories
-tis-mkfs-verbose
  • Provided by: Tis-mkfs :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in tis-mkfs
-tis-occurrence
  • Provided by: Find Occurrence
  • Type: set
  • Default: <none>
  • Categories: <none>
  • list all statements that may access lval
-tis-occurrence-statistics
  • Provided by: Find Occurrence
  • Type: boolean
  • Default: false
  • Opposite option: -no-tis-occurrence-statistics
  • enable statistics
-tis-print-deps
  • Provided by: Find Occurrence
  • Type: set
  • Default: <none>
  • Categories: <none>
  • print the dependencies of lval at the end of the entry point.
-tis-projects-clean
  • Provided by: Tis-projects
  • Type: boolean
  • Default: false
  • Opposite option: -tis-projects-no-clean
  • remove all projects except the current one. Can be used with -tis-projects-set-current which is applied first.
-tis-projects-debug
  • Provided by: Tis-projects :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in tis-projects
-tis-projects-help
  • Provided by: Tis-projects :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in tis-projects
-tis-projects-list
  • Provided by: Tis-projects
  • Type: boolean
  • Default: false
  • Opposite option: -tis-projects-no-list
  • print the list of the projects. The current project is marked with a *
-tis-projects-msg-key
  • Provided by: Tis-projects :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -tis-projects-msg-key help to get a list of available categories, and * to enable all categories
-tis-projects-set-current
  • Provided by: Tis-projects
  • Type: string
  • Default: <none>
  • set the current project to the specified one.
-tis-projects-verbose
  • Provided by: Tis-projects :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in tis-projects
-tis-review
  • Provided by: Server :: Analysis Configuration
  • Type: string
  • Default: <none>
  • Loads the Analysis Review settings from the given file. The settings can be obtained from the ‘Download config file’ button in the Analysis Review pane of the GUI.
-tis-review-auto-save
  • Provided by: Server :: Analysis Configuration
  • Type: boolean
  • Default: false
  • Opposite option: -no-tis-review-auto-save
  • When the option -tis-review is also set, the Analysis Review settings are automatically saved into the -tis-review option’s file when the program exits
-tis-utils-debug
  • Provided by: Tis-Utils :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Tis-Utils
-tis-utils-help
  • Provided by: Tis-Utils :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Tis-Utils
-tis-utils-msg-key
  • Provided by: Tis-Utils :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -tis-utils-msg-key help to get a list of available categories, and * to enable all categories
-tis-utils-verbose
  • Provided by: Tis-Utils :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Tis-Utils
-tty
  • Provided by: Kernel :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-tty
  • use terminal capabilities for feedback (when available)
-typecheck
  • Provided by: Kernel :: Checks
  • Type: boolean
  • Default: true
  • Opposite option: <none>
  • forces typechecking of the source files
-ulevel
  • Provided by: Kernel :: Customizing Normalization
  • Type: integer
  • Default: 0
  • unroll loops n times before analyzes. A negative value hides UNROLL loop pragmas.
-ulevel-force
  • Provided by: Kernel :: Customizing Normalization
  • Type: boolean
  • Default: false
  • Opposite option: -no-ulevel-force
  • ignore UNROLL loop pragmas disabling unrolling.
-undef-order-debug
  • Provided by: Undefined order :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in undefined order
-undef-order-help
  • Provided by: Undefined order :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in undefined order
-undef-order-msg-key
  • Provided by: Undefined order :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -undef-order-msg-key help to get a list of available categories, and * to enable all categories
-undef-order-verbose
  • Provided by: Undefined order :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in undefined order
-undefined-order-calls
  • Provided by: Undefined order
  • Type: boolean
  • Default: false
  • Opposite option: -no-undefined-order-calls
  • Check for undefined access orders including function calls. Implies -unspecified-access
-undefined-pointer-comparison-propagate-all
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: false
  • Opposite option: -no-undefined-pointer-comparison-propagate-all
  • if the target program appears to contain undefined pointer comparisons, propagate both outcomes {0; 1} in addition to the emission of an alarm
-unicode
  • Provided by: Kernel :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-unicode
  • use utf8 in messages
-unspecified-access
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-unspecified-access
  • do not assume that read/write accesses occurring between sequence points are separated
-users
  • Provided by: Users
  • Type: boolean
  • Default: false
  • Opposite option: -no-users
  • compute function callees
-users-debug
  • Provided by: Users :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in users
-users-help
  • Provided by: Users :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in users
-users-msg-key
  • Provided by: Users :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -users-msg-key help to get a list of available categories, and * to enable all categories
-users-verbose
  • Provided by: Users :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in users
-val
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-val
  • compute values
-val-args
  • Provided by: Value analysis :: Initial Context
  • Type: string
  • Default: <none>
  • Pass arguments to the entry point function. If the entry point has type int (int argc, char * argv[]), start analysis with argc bound to k+1 and argv pointing to a NULL-terminated array of pointers to strings “program”,”arg_1”,…, “arg_k”. The first character is used as separator to split the arguments, a space works well in the common cases.
-val-builtin
  • Provided by: Value analysis :: Precision vs. time
  • Type: map
  • Default: __builtin__exit:tis__exit, __builtin_acos:tis_acos, __builtin_alloca:tis_alloc, __builtin_asin:tis_asin, __builtin_atan2:tis_atan2, __builtin_atan:tis_atan, __builtin_ceil:tis_ceil, __builtin_ceilf:tis_ceilf, __builtin_cos:tis_cos, __builtin_exp:tis_exp, __builtin_expf:tis_expf, __builtin_floor:tis_floor, __builtin_floorf:tis_floorf, __builtin_fmax:tis_fmax, __builtin_fmin:tis_fmin, __builtin_fmod:tis_fmod, __builtin_log10:tis_log10, __builtin_log10f:tis_log10f, __builtin_log:tis_log, __builtin_logf:tis_logf, __builtin_malloc:tis_alloc, __builtin_memchr:tis_memchr, __builtin_memcmp:tis_memcmp, __builtin_memcpy:tis_memcpy, __builtin_memmove:tis_memmove, __builtin_memset:tis_memset, __builtin_pow:tis_pow, __builtin_powf:tis_powf, __builtin_printf:tis_printf, __builtin_round:tis_round, __builtin_roundf:tis_roundf, __builtin_sin:tis_sin, __builtin_snprintf:tis_snprintf, __builtin_sprintf:tis_sprintf, __builtin_sqrt:tis_sqrt, __builtin_sqrtf:tis_sqrtf, __builtin_strcat:tis_strcat, __builtin_strchr:tis_strchr, __builtin_strcmp:tis_strcmp, __builtin_strcpy:tis_strcpy, __builtin_strlen:tis_strlen, __builtin_strncat:tis_strncat, __builtin_strncmp:tis_strncmp, __builtin_strncpy:tis_strncpy, __builtin_tan:tis_tan, __builtin_trunc:tis_trunc, __builtin_truncf:tis_truncf, __builtin_vprintf:tis_vprintf, __builtin_vsnprintf:tis_vsnprintf, __builtin_vsprintf:tis_vsprintf, __builtin_wcslen:tis_wcslen, _exit:tis__exit, acos:tis_acos, alloca:tis_alloc, asin:tis_asin, atan2:tis_atan2, atan:tis_atan, ceil:tis_ceil, ceilf:tis_ceilf, cos:tis_cos, exp:tis_exp, expf:tis_expf, floor:tis_floor, floorf:tis_floorf, fmax:tis_fmax, fmin:tis_fmin, fmod:tis_fmod, free:tis_free, log10:tis_log10, log10f:tis_log10f, log:tis_log, logf:tis_logf, malloc:tis_alloc, memchr:tis_memchr, memcmp:tis_memcmp, memcpy:tis_memcpy, memmove:tis_memmove, memset:tis_memset, nan:tis_nan, nanf:tis_nanf, pow:tis_pow, powf:tis_powf, printf:tis_printf, realloc:tis_realloc, round:tis_round, roundf:tis_roundf, sin:tis_sin, snprintf:tis_snprintf, sprintf:tis_sprintf, sqrt:tis_sqrt, sqrtf:tis_sqrtf, strcat:tis_strcat, strchr:tis_strchr, strcmp:tis_strcmp, strcpy:tis_strcpy, strlen:tis_strlen, strncat:tis_strncat, strncmp:tis_strncmp, strncpy:tis_strncpy, strnlen:tis_strnlen, swprintf:tis_swprintf, tan:tis_tan, trunc:tis_trunc, truncf:tis_truncf, vprintf:tis_vprintf, vsnprintf:tis_vsnprintf, vsprintf:tis_vsprintf, vwprintf:tis_vwprintf, wcscat:tis_wcscat, wcschr:tis_wcschr, wcscmp:tis_wcscmp, wcscpy:tis_wcscpy, wcslen:tis_wcslen, wcsncat:tis_wcsncat, wcsncmp:tis_wcsncmp, wcsncpy:tis_wcsncpy, wcsnlen:tis_wcsnlen, wmemcpy:tis_wmemcpy, wmemmove:tis_wmemmove, wprintf:tis_wprintf
  • Categories: <none>
  • when analyzing function <f>, try to use TrustInSoft Kernel builtin <ffc> instead. Fall back to <f> if <ffc> cannot handle its arguments (experimental).
-val-callstack-results
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-callstack-results
  • record precisely the values before and after the evaluation of each statement for each callstack
-val-clone-on-recursive-calls
  • Provided by: Value analysis :: Deterministic programs
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-clone-on-recursive-calls
  • clone the called function when analyzing recursive calls. Only used when -val-ignore-recursive-calls is unset. The analysis has to be precise enought to be able to detect the termination (experimental)
-val-clone-on-recursive-calls-max-depth
  • Provided by: Value analysis :: Deterministic programs
  • Type: integer
  • Default: 100
  • Each recursive function is cloned at most n times.
-val-deterministic-nan
  • Provided by: Value analysis :: Deterministic programs
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-deterministic-nan
  • The NaN resulting of arithmetic operations is a quiet NaN with a 0 payload.
-val-dump-destination
  • Provided by: Value analysis :: Output Messages
  • Type: string
  • Default: txt
  • Possible values:all, json, none, txt
  • set the kind of output for the tis_dump_each_file calls.
-val-dump-directory
  • Provided by: Value analysis :: Output Messages
  • Type: string
  • Default: .
  • specify the directory where the dump file have to be stored
-val-exit-on-degeneration
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-exit-on-degeneration
  • if the value analysis degenerates, exit immediately with return code 2
-val-exit-on-reaching-max-mem
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-exit-on-reaching-max-mem
  • exit as fast as possible with code 124, whenever the Value Analysis allocates more memory than the environment variable TIS_KERNEL_MAX_MEM indicates. The value of this variable is set in GiB.
-val-ignore-recursive-calls
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-ignore-recursive-calls
  • Pretend function calls that would be recursive do not happen. Causes unsoundness
-val-ilevel
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 8
  • Possible values: between 4 and 512
  • Sets of integers are represented as sets up to <n> elements. Above, intervals with congruence information are used.
-val-initial-state
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-initial-state
  • compute initial state
-val-initial-state-print
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-initial-state-print
  • print results for option -val-initial-state
-val-initialization-padding-globals
  • Provided by: Value analysis :: Initial Context
  • Type: string
  • Default: yes
  • Possible values:maybe, no, yes
  • Specify how padding bits are initialized inside global variables. Possible values are <yes> (padding is fully initialized), <no> (padding is completely uninitialized), or <maybe> (padding may be uninitialized).
-val-int-for-pointer-equality
  • Provided by: Value analysis :: Propagation and alarms
  • Type: list
  • Default: <none>
  • -val-int-for-pointer-equality=n_1,n_2,…,n_k (k<=3) defines integer values n_1, n_2, …, n_k that valid pointers can be tested for equality against.
-val-interpreter-mode
  • Provided by: Value analysis :: Deterministic programs
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-interpreter-mode
  • Stop at first call to a library function, if main() has arguments, on undecided branches
-val-load-fun-state
  • Provided by: Value analysis :: Initial Context
  • Type: map
  • Default: <none>
  • Categories: <none>
  • load state of function <function> from file <filename>
-val-malloc-functions
  • Provided by: Value analysis
  • Type: set
  • Default: malloc, calloc, strdup, strndup
  • Categories: <none>
  • The allocation builtins use their call site to name new bases. This detection does not work for custom allocators or wrappers on top of malloc, unless they are listed here.
-val-malloc-plevel
  • Provided by: Value analysis
  • Type: integer
  • Default: 3
  • sets to [p] the number of precise dynamic allocation for any given callstack
-val-malloc-returns-null
  • Provided by: Value analysis
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-malloc-returns-null
  • The allocation built-ins are modeled as nondeterministically returning a null pointer
-val-print
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-print
  • print results for option -val
-val-print-callstacks
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-print-callstacks
  • When printing a message, also show the current call stack
-val-printf-accept-equisized-integral-types
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-printf-accept-equisized-integral-types
  • accept all integral types with the same size as the argument for ‘%[diuxXo]’ and their variants. This is an undefined behavior in all C standards, but it seems to have no observable consequences.
-val-printf-show-too-many-args
  • Provided by: Value analysis
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-printf-show-too-many-args
  • show a message when too many arguments are given to printf function.
-val-printf-singleton-pointers
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-printf-singleton-pointers
  • interpret ‘%p’ for singletons. Different pointers will be pretty-printed differently.
-val-profile
  • Provided by: Mode
  • Type: string
  • Default: analyzer
  • Define the Value Analysis profile to use, hence update a set of other command line options. Some profiles allow the usage of (comma-separated) flags, such as “interpreter:no-mem,no-builtin”. The available profiles (and their flags) can be listed with “-val-profile help”.
-val-program-name
  • Provided by: Value analysis :: Initial Context
  • Type: string
  • Default: program
  • Specify the name of the program.
-val-ptr-total-comparison
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-ptr-total-comparison
  • compare any two pointers, even if they have different bases, using a total and persistent order (works only if both pointers are precise and an ordering can be determined)
-val-reduce-on-logic-alarms
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-reduce-on-logic-alarms
  • Force reductions by a predicate to ignore logic alarms emitted while the predicated is evaluated (experimental)
-val-reset
  • Provided by: Value analysis :: Initial Context
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-reset
  • Remove all the generated alarms before starting another value analysis.
-val-reused-expressions
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-reused-expressions
  • undocumented
-val-save-fun-state
  • Provided by: Value analysis :: Initial Context
  • Type: map
  • Default: <none>
  • Categories: <none>
  • save state of function <function> in file <filename>
-val-show-allocations
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-show-allocations
  • Show memory allocations
-val-show-initial-state
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-show-initial-state
  • Show initial state before analysis starts
-val-show-perf
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-show-perf
  • Compute and shows a summary of the time spent analyzing function calls
-val-show-progress
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-show-progress
  • Show progression messages during analysis
-val-show-slevel
  • Provided by: Value analysis :: Output Messages
  • Type: integer
  • Default: 100
  • Period for showing consumption of the alloted slevel during analysis
-val-show-trace
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-show-trace
  • Compute and display execution traces together with alarms (experimental)
-val-simple-stubs
  • Provided by: Value analysis :: Initial Context
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-simple-stubs
  • Assume that undefined functions returning pointers always return NULL.
-val-skip-inclusion-check
  • Provided by: Value analysis :: Deterministic programs
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-skip-inclusion-check
  • Disable inclusion checks during the entire value analysis. Inclusion checks are part of the guarantee that the analyzer terminates for target programs that terminate and for target programs that do not, so they should generally not be skipped. However, users very familiar with the value analysis may be able to recognize on sight target code for which this check is not necessary, and disable the check to improve speed.
-val-skip-inclusion-check-function
  • Provided by: Value analysis :: Deterministic programs
  • Type: set
  • Default: <none>
  • Categories: all
  • Disable inclusion checks while analyzing function f
-val-slevel-merge-after-loop
  • Provided by: Value analysis :: Precision vs. time
  • Type: set
  • Default: @all, -__mkfs_get_file, -__mkfs_get_dir
  • Categories: all
  • when set, the different execution paths that originate from the body of a loop are merged before entering the next execution. Experimental.
-val-slevel-results
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-slevel-results
  • store states by slevel (before state only)
-val-split-return
  • Provided by: Value analysis :: Precision vs. time
  • Type: string
  • Default: <none>
  • when ‘mode’ is a number, or ‘full’, this is equivalent to -val-split-return-function f:mode for all functions f. When mode is ‘auto’, automatically split states at the end of all functions, according to the function return code.
-val-split-return-function
  • Provided by: Value analysis :: Precision vs. time
  • Type: map
  • Default: __mkfs_get_file:full, __mkfs_get_dir:full, calloc:full, setenv:auto, local_putenv:full, tis_nondet_ptr:full
  • Categories: <none>
  • split return states of function <f> according to result == n and result != n
-val-statistics
  • Provided by: Value analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-statistics
  • Measure analysis time for statements and functions
-val-stop-at-nth-alarm
  • Provided by: Value analysis :: Deterministic programs
  • Type: integer
  • Default: <none>
-val-stop-at-nth-garbled
  • Provided by: Value analysis :: Deterministic programs
  • Type: integer
  • Default: 0
  • Stop after having evaluated n expressions which yield a garbled mix of addresses. Currently, only values 0 and 1 are supported
-val-stop-on-pointer-library-function
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -val-continue-on-pointer-library-function
  • Stop the analysis as soon as a library function returning a pointer type is encountered
-val-stop-on-throwing-library-function
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -val-continue-on-throwing-library-function
  • Stop the analysis as soon as a library function which may throw an exception is encountered
-val-subdivide-non-linear
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 0
  • Improve precision when evaluating expressions in which a variable appears multiple times, by splitting its value at most n times. Experimental.
-val-tis-alloc-weak-size
  • Provided by: Value analysis
  • Type: integer
  • Default: 10000
  • sets the size of the location returned by tis_alloc_weak_legacy to [p] for any given callstack
-val-tis-check-included-stop-at-first
  • Provided by: Value analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-val-tis-check-included-stop-at-first
  • Stop on the first memory chunk that is not included into another one
-val-use-spec
  • Provided by: Value analysis :: Precision vs. time
  • Type: set
  • Default: <none>
  • Categories: all
  • use the ACSL specification of the functions instead of their definitions
-val-warn-copy-indeterminate
  • Provided by: Value analysis :: Propagation and alarms
  • Type: set
  • Default: <none>
  • Categories: all
  • warn when a statement of the specified functions copies a value that may be indeterminate (uninitalized or containing escaping address). Any number of function may be specified. If @all’ is present, this option becomes active for all functions. Inactive by default.
-val-warn-harmless-function-pointers
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-warn-harmless-function-pointers
  • Warn for harmless mismatches between function pointer type and called function.
-val-warn-left-shift-negative
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-warn-left-shift-negative
  • Emit alarms when left-shifting negative integers
-val-warn-pointer-arithmetic-out-of-bounds
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-warn-pointer-arithmetic-out-of-bounds
  • Warn when adding an offset to a pointer produces an out-of-bounds pointer. When unset, do not warn but generate &a-1, &a+2…
-val-warn-pointer-subtraction
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-warn-pointer-subtraction
  • Warn when subtracting two pointers that may not be in the same allocated block, and return the pointwise difference between the offsets. When unset, do not warn but generate imprecise offsets.
-val-warn-undefined-pointer-comparison
  • Provided by: Value analysis :: Propagation and alarms
  • Type: string
  • Default: all
  • Possible values:all, none, pointer
  • warn on all pointer comparisons (default), on comparisons where the arguments have pointer type, or never warn
-val-warn-va-arg-type-mismatch
  • Provided by: Value analysis :: Propagation and alarms
  • Type: boolean
  • Default: true
  • Opposite option: -no-val-warn-va-arg-type-mismatch
  • Warn for mismatches between the type parameter passed to the va_arg macro and the actual type of the next variadic argument.
-value-debug
  • Provided by: Value analysis :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in value analysis
-value-help
  • Provided by: Value analysis :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in value analysis
-value-messages
  • Provided by: Server
  • Type: boolean
  • Default: false
  • Opposite option: -no-value-messages
  • keep all Value messages for the GUI. This option can greatly increase the state saved on the disk with the option -save
-value-msg-key
  • Provided by: Value analysis :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -value-msg-key help to get a list of available categories, and * to enable all categories
-value-verbose
  • Provided by: Value analysis :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in value analysis
-verbose
  • Provided by: Kernel :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= -1
  • general level of verbosity
-volatile
  • Provided by: Volatile
  • Type: boolean
  • Default: false
  • Opposite option: -no-volatile
  • builds a new projet (named “Volatile”) where volatile access are simulated by function calls
-volatile-debug
  • Provided by: Volatile :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in Volatile
-volatile-globals
  • Provided by: Kernel :: Analysis Options
  • Type: set
  • Default: <none>
  • Categories: <none>
  • force the given set of global variables to behave like fully volatile variables. Use NULL for absolute memory.
-volatile-help
  • Provided by: Volatile :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in Volatile
-volatile-msg-key
  • Provided by: Volatile :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -volatile-msg-key help to get a list of available categories, and * to enable all categories
-volatile-verbose
  • Provided by: Volatile :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in Volatile
-volatile-version
  • Provided by: Volatile
  • Type: boolean
  • Default: false
  • Opposite option: -volatile-no-version
  • prints plugin version
-vres-debug
  • Provided by: Resume :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in resume
-vres-help
  • Provided by: Resume :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in resume
-vres-msg-key
  • Provided by: Resume :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -vres-msg-key help to get a list of available categories, and * to enable all categories
-vres-slevel
  • Provided by: Resume
  • Type: integer
  • Default: <none>
  • change value of -slevel after a value analysis has been stopped
-vres-verbose
  • Provided by: Resume :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in resume
-warn-decimal-float
  • Provided by: Kernel :: Parsing
  • Type: string
  • Default: none
  • Possible values:all, none, once
  • Warn when floating-point constants cannot be exactly represented; freq must be one of none, once or all
-warn-signed-downcast
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-warn-signed-downcast
  • generate alarms when signed downcasts may exceed the destination range
-warn-signed-overflow
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: true
  • Opposite option: -no-warn-signed-overflow
  • generate alarms for signed operations that overflow.
-warn-unsigned-downcast
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-warn-unsigned-downcast
  • generate alarms when unsigned downcasts may exceed the destination range
-warn-unsigned-overflow
  • Provided by: Kernel :: Analysis Options
  • Type: boolean
  • Default: false
  • Opposite option: -no-warn-unsigned-overflow
  • generate alarms for unsigned operations that overflow
-warning-on-lvalues-partially-volatile
  • Provided by: Volatile
  • Type: boolean
  • Default: true
  • Opposite option: -no-warning-on-lvalues-partially-volatile
  • warns on accesses to lvalues partially volatile
-warning-on-volatile-casts
  • Provided by: Volatile
  • Type: boolean
  • Default: true
  • Opposite option: -no-warning-on-volatile-casts
  • warns on casts which may loose volatile qualifier
-warning-on-volatile-lvalues
  • Provided by: Volatile
  • Type: boolean
  • Default: true
  • Opposite option: -no-warning-on-volatile-lvalues
  • warns on accesses to lvalues completely volatile
-whole-program-deps
  • Provided by: From analysis
  • Type: boolean
  • Default: false
  • Opposite option: -no-whole-program-deps
  • Compute whole program dependencies. Incompatible with memexec.
-whole-program-deps-print
  • Provided by: From analysis :: Output Messages
  • Type: boolean
  • Default: true
  • Opposite option: -no-whole-program-deps-print
  • print results for option -whole-program-deps
-whole-program-graph
  • Provided by: Value analysis :: Results memoization vs. time
  • Type: boolean
  • Default: false
  • Opposite option: -no-whole-program-graph
  • Compute a whole-program result graph (needed for some plugins)
-wholegraph-debug
  • Provided by: Whole program graph utilities :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in whole program graph utilities
-wholegraph-help
  • Provided by: Whole program graph utilities :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in whole program graph utilities
-wholegraph-msg-key
  • Provided by: Whole program graph utilities :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -wholegraph-msg-key help to get a list of available categories, and * to enable all categories
-wholegraph-verbose
  • Provided by: Whole program graph utilities :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in whole program graph utilities
-wlevel
  • Provided by: Value analysis :: Precision vs. time
  • Type: integer
  • Default: 3
  • do <n> loop iterations before widening
-wp
  • Provided by: WP :: Goal Selection
  • Type: boolean
  • Default: false
  • Opposite option: -no-wp
  • Generate proof obligations for all (selected) properties.
-wp-alias-vars
  • Provided by: WP :: Model Selection
  • Type: set
  • Default: <none>
  • Categories: <none>
  • Consider variable names aliased.
-wp-alt-ergo
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: alt-ergo
  • Command to run alt-ergo
-wp-alt-ergo-lib
  • Provided by: WP :: Prover Options
  • Type: list
  • Default: <none>
  • Additional library file for Alt-Ergo
-wp-alt-ergo-opt
  • Provided by: WP :: Prover Options
  • Type: list
  • Default: <none>
  • Additional options for Alt-Ergo
-wp-altgr-ergo
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: altgr-ergo
  • Command to run alt-ergo user interface
-wp-auto
  • Provided by: WP :: Prover Interface
  • Type: list
  • Default: <none>
  • Activate auto-search with strategy <s>. Implies -wp-prover ‘tip’. Use ‘-wp-prover ?’ for listing strategies.
-wp-auto-backtrack
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 0
  • Backtracking limit (-wp-auto only, de-activated by default). Limits backtracking when applying strategies.
-wp-auto-depth
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 5
  • Depth of auto-search (-wp-auto only, default 5). Limits the number of nested level in strategies.
-wp-auto-width
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 10
  • Width of auto-search (-wp-auto only, default 10). Limits the number of pending goals in strategies.
-wp-bhv
  • Provided by: WP :: Goal Selection
  • Type: list
  • Default: <none>
  • Select properties of the given behaviors (defaults to all behaviors) of the selected functions.
-wp-bits
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-bits
  • Use bit-test simplifications.
-wp-bool-range
  • Provided by: WP :: Model Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-bool-range
  • Assumes _Bool values have no trap representations.
-wp-bound-forall-unfolding
  • Provided by: WP :: Qed Simplifications
  • Type: integer
  • Default: 1000
  • Instantiate up to <n> forall-integers hypotheses.
-wp-callee-precond
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-callee-precond
  • Use pre-conditions of callee.
-wp-check
  • Provided by: WP :: Proof Obligations
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-check
  • Check the syntax and type of the produced file, instead of proving.
-wp-clean
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-clean
  • Use a simple cleaning in case of -wp-no-let.
-wp-context-vars
  • Provided by: WP :: Model Selection
  • Type: set
  • Default: <none>
  • Categories: <none>
  • Consider variable names in isolated context.
-wp-coq-lib
  • Provided by: WP :: Prover Options
  • Type: list
  • Default: <none>
  • Additional libraries for Coq
-wp-coq-project
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: _CoqProject
  • Set the Coq-Project file to used with Proof General
-wp-coq-timeout
  • Provided by: WP :: Prover Options
  • Type: integer
  • Default: 30
  • Set the timeout (in seconds) for Coq.
-wp-coqc
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: coqc
  • Set the command line to run Coq Compiler.
-wp-coqide
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: coqide
  • Set the command line to run CoqIde If the command-line contains ‘emacs’ (case insentive), a coq-project file is used instead of coq options.
-wp-core
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-core
  • Lift core facts through branches.
-wp-debug
  • Provided by: WP :: Output Messages
  • Type: integer
  • Default: 0
  • Possible values: integers >= 0
  • level of debug for plug-in WP
-wp-depth
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 0
  • Set depth of exploration for provers.
-wp-detect
  • Provided by: WP :: Prover Interface
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-detect
  • List installed provers.
-wp-driver
  • Provided by: WP :: Prover Interface
  • Type: list
  • Default: <none>
  • Load drivers for linking to external libraries
-wp-dynamic
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-dynamic
  • Handle dynamic calls with specific annotations.
-wp-extensional
  • Provided by: WP :: Model Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-extensional
  • Use extensional equality on compounds (hypotheses only).
-wp-extern-arrays
  • Provided by: WP :: Model Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-extern-arrays
  • Put some default size for extern arrays.
-wp-fct
  • Provided by: WP :: Goal Selection
  • Type: set
  • Default: <none>
  • Categories: all
  • Select properties of given functions (defaults to all functions).
-wp-filename-truncation
  • Provided by: WP :: Proof Obligations
  • Type: integer
  • Default: 60
  • Truncate basename of proof obligation files after <n> characters. Since numbers can be added as suffixes to make theses names unique, filename lengths can be highter to <n>. No truncation is performed when the value equals to zero.
-wp-filter
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-filter
  • Use variable filtering.
-wp-gen
  • Provided by: WP :: Prover Interface
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-gen
  • Only generate prover files.
-wp-ground
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-ground
  • Use aggressive ground simplifications.
-wp-help
  • Provided by: WP :: Getting Information
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • help of plug-in WP
-wp-hints
  • Provided by: WP :: Prover Options
  • Type: integer
  • Default: 3
  • Maximum number of proposed Coq scripts
-wp-include
  • Provided by: WP :: Prover Options
  • Type: list
  • Default: <none>
  • Directory where to find libraries and drivers for provers
-wp-init-alias
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-init-alias
  • Use initializers for aliasing propagation.
-wp-init-const
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-init-const
  • Use initializers for global const variables.
-wp-init-summarize-array
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-init-summarize-array
  • Summarize contiguous initializers with quantifiers.
-wp-let
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-let
  • Use variable elimination.
-wp-literals
  • Provided by: WP :: Model Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-literals
  • Export content of string literals.
-wp-model
  • Provided by: WP :: Model Selection
  • Type: list
  • Default: <none>
  • Memory model selection. Available selectors:
    • ‘Hoare’ logic variables only
    • ‘Typed’ typed pointers only
    • ‘+nocast’ no pointer cast
    • ‘+cast’ unsafe pointer casts
    • ‘+raw’ no logic variable
    • ‘+ref’ by-reference-style pointers detection
    • ‘+nat/+int’ natural or machine-integers arithmetics
    • ‘+real/+float’ real or IEEE floating point arithmetics
-wp-msg-key
  • Provided by: WP :: Output Messages
  • Type: set
  • Default: <none>
  • Categories: <none>
  • enables message display for categories <k1>,…,<kn>. Use -wp-msg-key help to get a list of available categories, and * to enable all categories
-wp-out
  • Provided by: WP :: Proof Obligations
  • Type: string
  • Default: <none>
  • Set working directory for generated files. Defaults to some temporary directory.
-wp-overflows
  • Provided by: WP :: Model Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-overflows
  • Collect hypotheses for absence of overflow and downcast (incompatible with RTE generator plug-in)
-wp-par
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 4
  • Number of parallel proof processes.
-wp-parasite
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-parasite
  • Use singleton-variable filtering.
-wp-prenex
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-prenex
  • Normalize nested foralls into prenex-form
-wp-print
  • Provided by: WP :: Proof Obligations
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-print
  • Pretty-prints proof obligations on standard output.
-wp-print-unsolved
  • Provided by: WP :: Proof Obligations
  • Type: boolean
  • Default: false
  • Opposite option: <none>
  • Pretty-prints unsolved proof obligations on standard output.
-wp-proof-trace
  • Provided by: WP :: Prover Interface
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-proof-trace
  • Keeps output of provers for valid POs.
-wp-prop
  • Provided by: WP :: Goal Selection
  • Type: list
  • Default: <none>
  • Select properties having the one of the given tagnames (defaults to all properties). You may also replace the tagname by @category’ for the selection of all properties of the given category. Accepted categories are: lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors, assert, invariant, variant, breaks, continues, returns, calls. Prepend a minus sign (-) to remove properties from the selection.
-wp-prover
  • Provided by: WP :: Prover Interface
  • Type: list
  • Default: <none>
  • Submit proof obligations to external prover(s):
    • ‘none’ to skip provers
    • ‘script’ (session scripts only)
    • ‘tip’ (failed scripts only)
    • ‘alt-ergo’ (default)
    • ‘altgr-ergo’ (gui)
    • ‘coq’, ‘coqide’ (see also -wp-script)
    • ‘why3:<dp>’ or ‘<dp>’ (why3 prover, see -wp-detect)
    • ‘why3ide’ (why3 gui)
-wp-pruning
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-pruning
  • Prune trivial branches.
-wp-qed-checks
  • Provided by: WP :: Qed Simplifications
  • Type: set
  • Default: <none>
  • Categories: <none>
  • Check internal simplifications.
-wp-reduce
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-reduce
  • Reduce function equalities with precedence to constructors.
-wp-ref-vars
  • Provided by: WP :: Model Selection
  • Type: set
  • Default: <none>
  • Categories: <none>
  • Consider variable names by reference.
-wp-report
  • Provided by: WP :: Proof Obligations
  • Type: list
  • Default: <none>
  • Report specification file(s)
-wp-report-basename
  • Provided by: WP :: Proof Obligations
  • Type: string
  • Default: wp-report
  • Basename of generated reports
-wp-report-json
  • Provided by: WP :: Proof Obligations
  • Type: string
  • Default: <none>
  • Output report in json format into given file. If the file already exists, it is used for stabilizing range of steps in other reports.
-wp-rte
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-rte
  • Generate RTE guards before WP.
-wp-script
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: <none>
  • Set user’s file for Coq proofs.
-wp-session
  • Provided by: WP
  • Type: string
  • Default: <none>
  • set the plug-in session directory to <dir>
-wp-share
  • Provided by: WP
  • Type: string
  • Default: <none>
  • set the plug-in share directory to <dir> (may be used if the plug-in is not installed at the same place as TrustInSoft Kernel)
-wp-simpl
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-simpl
  • Enable Qed Simplifications.
-wp-simplify-forall
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-simplify-forall
  • Remove machine integer ranges in quantifiers.
-wp-simplify-is-cint
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-simplify-is-cint
  • Remove redundant machine integer range hypothesis.
-wp-simplify-land-mask
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-simplify-land-mask
  • Tight logical masks on unsigned integers.
-wp-simplify-type
  • Provided by: WP :: Qed Simplifications
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-simplify-type
  • Remove all Type constraints.
-wp-skip-fct
  • Provided by: WP :: Goal Selection
  • Type: set
  • Default: <none>
  • Categories: all
  • Skip the specified functions (defaults to none).
-wp-split
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-split
  • Split conjunctions into sub-goals.
-wp-split-depth
  • Provided by: WP :: Computation Strategies
  • Type: integer
  • Default: 0
  • Set depth of exploration for splitting conjunctions into sub-goals. Value -1 means an unlimited depth.
-wp-status-all
  • Provided by: WP :: Goal Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-status-all
  • Select properties with any status.
-wp-status-invalid
  • Provided by: WP :: Goal Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-status-invalid
  • Select properties with status ‘Invalid’.
-wp-status-maybe
  • Provided by: WP :: Goal Selection
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-status-maybe
  • Select properties with status ‘Maybe’.
-wp-status-valid
  • Provided by: WP :: Goal Selection
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-status-valid
  • Select properties with status ‘Valid’.
-wp-steps
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 0
  • Set number of steps for provers.
-wp-tactic
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: auto with zarith
  • Default tactic for Coq
-wp-time-extra
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 5
  • Set extra-time (in seconds) for proof replay.
-wp-time-margin
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 2
  • Set margin-time (in seconds) for considering a proof automatic. When using the ‘tip’ prover, scripts are created or cancelled if the proof time is greater or lower than (timeout - margin)..
-wp-timeout
  • Provided by: WP :: Prover Interface
  • Type: integer
  • Default: 10
  • Set the timeout (in seconds) for provers.
-wp-tryhints
  • Provided by: WP :: Prover Options
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-tryhints
  • Try scripts from other goals (see also -wp-hints)
-wp-unalias-vars
  • Provided by: WP :: Model Selection
  • Type: set
  • Default: <none>
  • Categories: <none>
  • Consider variable names non-aliased.
-wp-unfold-assigns
  • Provided by: WP :: Computation Strategies
  • Type: boolean
  • Default: false
  • Opposite option: -wp-no-unfold-assigns
  • Unfold aggregates in assigns.
-wp-update-script
  • Provided by: WP :: Prover Options
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-update-script
  • If turned off, do not save or modify user’s proofs.
-wp-verbose
  • Provided by: WP :: Output Messages
  • Type: integer
  • Default: 1
  • Possible values: integers >= 0
  • level of verbosity for plug-in WP
-wp-volatile
  • Provided by: WP :: Model Selection
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-volatile
  • Sound modeling of volatile access. Use -wp-no-volatile to ignore volatile attributes.
-wp-warn-separation
  • Provided by: WP :: Proof Obligations
  • Type: boolean
  • Default: true
  • Opposite option: -wp-no-warn-separation
  • Warn Against Separation Hypotheses
-wp-why-lib
  • Provided by: WP :: Prover Options
  • Type: list
  • Default: <none>
  • Additional libraries for Why
-wp-why-opt
  • Provided by: WP :: Prover Options
  • Type: list
  • Default: <none>
  • Additional options for Why3
-wp-why3
  • Provided by: WP :: Prover Options
  • Type: string
  • Default: why3
  • Command to run Why-3

Undocumented options

Some options that are not referenced yet in the user manual.