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¶

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:

the name of the option
- the name of the feature providing the option
- the type of the option
- the default value of the option (if any)
- the name of the opposite option (for Boolean type options only)
- the list of available Categories if enabled (for List type options and Set type options only)
- the description of the option

–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

-16

Provided by: Kernel :: Parsing
Type: boolean
Default: false
Opposite option: <none>
Alias for -machdep=gcc_x86_16

-32

Provided by: Kernel :: Parsing
Type: boolean
Default: false
Opposite option: <none>
Alias for -machdep=gcc_x86_32

-64

Provided by: Kernel :: Parsing
Type: boolean
Default: false
Opposite option: <none>
Alias for -machdep=gcc_x86_64

-D

Provided by: Kernel :: Parsing
Type: string
Default: <none>
Alias for -cpp-extra-args=”-D <macro>” and -cxx-cpp-extra-args=”-D <macro>”

-I

Provided by: Kernel :: Parsing
Type: string
Default: <none>
Alias for -cpp-extra-args=”-I <dir>” and -cxx-cpp-extra-args=”-I <dir>”

-U

Provided by: Kernel :: Parsing
Type: string
Default: <none>
Alias for -cpp-extra-args=”-U <macro>” and -cxx-cpp-extra-args=”-U <macro>”

-absolute-address

Provided by: Kernel :: Analysis Options
Type: map
Default: <none>
Categories: <none>
Constrain a set of global variables to specific absolute addresses or to ranges of addresses with optional alignment.

A constraint is expressed as a name of a variable and either a precise address or a range. Constraints for multiple variables form a comma-separated list.

A precise address is expressed as a 64-bit integer in decimal, hexadecimal (‘0x’, ‘0X’), octal (‘0o’, ‘0O’), or binary (‘0b’, ‘0B’) notation, e.g.:
```
-absolute-address=x:0x01,y:0x3f
```
A range is expressed through its inclusive boundaries ‘[START_ADDR..END_ADDR]’ where ‘START_ADDR’ and ‘END_ADDR’ are precise addresses, e.g.:
```
-absolute-address=x:[0x01..0x3f]
```
A range can also be expressed as a reference to a named memory region (see -memory-region), e.g.:
```
-absolute-address=x:R -memory-region=R:0x01[64]
```
Ranges can be further constrained to an alignment by providing a congruence declaration after a backslash-escaped comma, e.g.:
```
-absolute-address=x:[0x01..0x3f]\,2%4
-absolute-address=x:R\,0%4 -memory-region=R:0x01[64]
```
Constraints cannot include the address ‘0x0’. The set of constraints must be such that each variable can be assigned an address that is unique and that does not cause it to overlap with other variables or the absolute valid range (see option -absolute-valid-range).

See TrustInSoft User Guide on Dealing with special features (Physical addresses) for more information.

-absolute-valid-range

Provided by: Kernel :: Analysis Options
Type: string
Default: <none>
Treat accesses to absolute addresses within the specified range as valid.

Range is specified as min and max, both expressed as 64-bit integers in decimal, hexadecimal (‘0x’, ‘0X’), octal (‘0o’, ‘0O’), or binary (‘0b’, ‘0B’) notation. Example:
```
-absolute-valid-range=0x01-0x3f
```
All accesses to absolute addresses within this range are valid and all absolute addresses outside of it are invalid. In the absence of this option, all absolute addresses are assumed to be invalid.

See TrustInSoft User Guide on Dealing with special features (Physical addresses) for more information.

-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 casts from integer to C integral types and makes them explicit

-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
Assume all base addresses are divisible by N.

N can take the form of an integer, e.g.:
```
-address-alignment=4
```
The alignment set with -address-alignment is overridden by address constraints specified with -absolute-address and the ‘tis_address’ attribute.

See TrustInSoft User Guide on Dealing with special features (Physical addresses) for more information.

-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
Automatically replace accesses to volatile variables with function calls based on the type of those volatile variables. Used in conjunction with -volatile.

Functions are automatically bound to specific volatile variables based of the functions’ names and signatures.For a variable of type TYPE, read accesses and write accesses are replaced with functions with names and signatures of the following form:

TYPE c2fc2_Rd_TYPE(TYPE *ptr);

TYPE c2fc2_Wr_TYPE(TYPE *ptr, TYPE value);

“c2fc2_” is a prefix string that can be specified by the option -binding-prefix.

If no compatible function exists for a given type, the analyzer proceeds as normal, but without replacing the accesses to variables of that type. If a variable is already bound to a specific function because of a declaration in the source code, the declaration takes precedence over automated binding.

Use the following options to debug the binding process and see actual function names being bound:
```
-debug=2 -volatile-msg-key=binding
```
See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-binding-prefix

Provided by: Volatile
Type: string
Default: c2fc2_
Set the prefix used in function names during automatic binding when replacing accesses to volatile variables with function calls. Used in conjunction with -binding-auto.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-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: <none>
<cmd> is used to build the preprocessing command. Default to $CPP environment variable or else “clang -E -C -nostdinc”. 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_MAJOR__=X, -D__TRUSTINSOFT_MINOR__=Y, -D__TRUSTINSOFT_PATCH__=Z -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-custom-isystem

Provided by: CXX
Type: list
Default: <none>
Add additional paths to the preprocessor standard system directories, before the default ones.

-cxx-debug

Provided by: CXX :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in CXX

-cxx-debug-convert-name

Provided by: FIR to Cabs translator
Type: string
Default: <none>
print the FIR representation of [qname] before translating it to CABS, and print the result afterwards. The format to use for [qname] is ‘std::foo::Bar’.

-cxx-debug-fir

Provided by: FIR to Cabs translator
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-fir-name

Provided by: FIR to Cabs translator
Type: string
Default: <none>
print only the FIR declarations with the qualified name [qname] when using -cxx-debug-fir. The format to use for [qname] is ‘std::foo::Bar’.

-cxx-debug-graph

Provided by: FIR to Cabs translator
Type: string
Default: <none>
dump a <template>.svg file with its <template>.dot file and a <template>.txt file with id-name associations

-cxx-debug-reorder

Provided by: FIR to Cabs translator
Type: string
Default: <none>
print the constraints required to reorder the entity [qname]. The format to use for [qname] is ‘std::foo::Bar’.

-cxx-debug-vmt

Provided by: FIR to Cabs translator
Type: string
Default: <none>
print debugging information about the generation of the virtual method of the class [qname]. The format to use for [qname] is ‘std::foo::Bar’.

-cxx-demangling-full

Provided by: CXX
Type: boolean
Default: false
Opposite option: <none>
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-fir-type-profile

Provided by: FIR to Cabs translator
Type: list
Default: <none>
Displays the FIR profile for the requested shared types.

-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-inline-virtual-calls

Provided by: CXX
Type: boolean
Default: true
Opposite option: -no-cxx-inline-virtual-calls
Inline virtual call adjustments in the generated code..

-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: false
Opposite option: -no-cxx-odr-optimize
Replace ODR-duplicate definitions by declarations.

-cxx-parse-only

Provided by: CXX
Type: boolean
Default: false
Opposite option: -no-cxx-parse-only
Get only the diagnostics but do not produce code.

-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. Deprecated since this information is now available in tis-aggregate.

-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>

-edom-value

Provided by: Kernel :: Analysis Options
Type: integer
Default: 1
The EDOM errno value. This value must match the value defined in the header files used for the analysis.

-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

-fir-debug

Provided by: FIR to Cabs translator :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in FIR to Cabs translator

-fir-help

Provided by: FIR to Cabs translator :: Getting Information
Type: boolean
Default: false
Opposite option: <none>
help of plug-in FIR to Cabs translator

-fir-msg-key

Provided by: FIR to Cabs translator :: Output Messages
Type: set
Default: <none>
Categories: <none>
enables message display for categories <k1>,…,<kn>. Use -fir-msg-key help to get a list of available categories, and * to enable all categories

-fir-verbose

Provided by: FIR to Cabs translator :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in FIR to Cabs translator

-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

-gtest

Provided by: CXX
Type: boolean
Default: false
Opposite option: -no-gtest
Adds runtime files and includes for GoogleTest.

-gtest-main

Provided by: CXX
Type: boolean
Default: false
Opposite option: -no-gtest-main
Adds runtime files and includes for GoogleTest, as well as the test driver used when linking against the gtest_main library.

-gui

Provided by: Server :: Web Server Configuration
Type: boolean
Default: false
Opposite option: -no-gui
Start the GUI so it becomes available from a web browser

-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

-help-option

Provided by: Kernel :: Getting Information
Type: string
Default: <none>
Display a detailed help for the given option.

-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-dead

Provided by: Info :: CSV generation
Type: string
Default: <none>
export information about dead blocks in the specified csv file.

-info-csv-decisions

Provided by: Info :: CSV generation
Type: string
Default: <none>
export information about decisions in the specified csv file

-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-dead

Provided by: Info
Type: boolean
Default: false
Opposite option: -info-no-dead
print information about dead blocks.

-info-debug

Provided by: Info :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in info

-info-decisions

Provided by: Info
Type: boolean
Default: false
Opposite option: -info-no-decisions
print information about decisions

-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-dead

Provided by: Info :: Getting Information
Type: boolean
Default: false
Opposite option: -info-no-help-dead
print help about getting information about dead blocks.

-info-help-decisions

Provided by: Info :: Getting Information
Type: boolean
Default: false
Opposite option: -info-no-help-decisions
print help about getting information about decisions.

-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

-isystem

Provided by: Kernel :: Parsing
Type: string
Default: <none>
Alias for -cpp-extra-args=”-isystem <dir>” and -cxx-cpp-extra-args=”-isystem <dir>”

-j3

Provided by: J3 :: Goals Generation
Type: boolean
Default: false
Opposite option: -no-j3
Generate proof obligations for all (selected) properties.

-j3-ae-steps

Provided by: J3 :: Provers configuration
Type: integer
Default: 0
Set a steps limit for alt-ergo. Use 0 for no steps limit.

-j3-bv

Provided by: J3 :: Goals Generation
Type: boolean
Default: true
Opposite option: -j3-no-bv
Use bitvectors to represent integers.

-j3-cex

Provided by: J3 :: Counterexamples
Type: boolean
Default: false
Opposite option: -j3-no-cex
Ask for counterexamples when possible.

-j3-cex-entry-point

Provided by: J3 :: Counterexamples
Type: boolean
Default: false
Opposite option: -j3-no-cex-entry-point
Only print the counterexample at the entry point.

-j3-check-termination

Provided by: J3 :: Goals Generation
Type: boolean
Default: false
Opposite option: -j3-no-check-termination
Check the termination of functions.

-j3-cvc4-steps

Provided by: J3 :: Provers configuration
Type: integer
Default: 0
Set a steps limit for CVC4. Use 0 for no steps limit.

-j3-cvc5-steps

Provided by: J3 :: Provers configuration
Type: integer
Default: 0
Set a steps limit for cvc5. Use 0 for no steps limit.

-j3-debug

Provided by: J3 :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in J3

-j3-exact-float

Provided by: J3 :: Goals Generation
Type: boolean
Default: false
Opposite option: -j3-no-exact-float
Activate support for exact and round_error in ACSL annotations, using a ghost real representation of floating-point computations.

-j3-extra-config

Provided by: J3 :: Why3 configuration
Type: list
Default: <none>
Add an extra configuration file for Why3.

-j3-fast

Provided by: J3 :: Goals Generation
Type: boolean
Default: true
Opposite option: -j3-no-fast
Use the fast WP mode. It generates fewer goals and avoids combinatorial explosions with complex programs through the use of the Strongest Postcondition variant of the WP calculus.

-j3-fct

Provided by: J3 :: Goals Generation
Type: set
Default: <none>
Categories: all
Limit the analysis to a set of functions.

-j3-help

Provided by: J3 :: Getting Information
Type: boolean
Default: false
Opposite option: <none>
help of plug-in J3

-j3-load-path

Provided by: J3 :: Why3 configuration
Type: list
Default: <none>
Add a path to the Why3 load path.

-j3-logic

Provided by: J3 :: Goals Generation
Type: boolean
Default: true
Opposite option: -j3-no-logic
Prove the lemmas.

-j3-max-provers

Provided by: J3 :: Provers configuration
Type: integer
Default: <none>
Define the number of provers that can run at the same time. Default is the number defined in the .why3.conf file.

-j3-memlimit

Provided by: J3 :: Provers configuration
Type: integer
Default: 4000
Set a memory limit in MB for all the provers. Use 0 for no memlimit.

-j3-mlw

Provided by: J3 :: Debug
Type: string
Default: <none>
output file for intermediate Why3 code.

-j3-msg-key

Provided by: J3 :: Output Messages
Type: set
Default: <none>
Categories: <none>
enables message display for categories <k1>,…,<kn>. Use -j3-msg-key help to get a list of available categories, and * to enable all categories

-j3-prop

Provided by: J3 :: Goals Generation
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, allocates, frees, ub. Prepend a minus sign (-) to remove properties from the selection. A property is selected if one of its names is included and none if its names is excluded. If there are only excluded names, all other names are considered included by default. The order of this list does not matter.

-j3-provers

Provided by: J3 :: Provers configuration
Type: set
Default: <none>
Categories: <none>
Select a specific prover. The selected provers can be used for the proof instead of the standard provers. (advanced users only).

-j3-safe-float

Provided by: J3 :: Goals Generation
Type: boolean
Default: false
Opposite option: -j3-no-safe-float
Restrict the floating point domain to finite floats. All floats are assumed to be finite. The basic arithmetic operations on floats come with preconditions ensuring that their result is finite. The cast from reals to floats also has a similar precondition.

-j3-save-session

Provided by: J3 :: Why3 configuration
Type: boolean
Default: false
Opposite option: -j3-no-save-session
Save the Why3 session after a proof.

-j3-share

Provided by: J3
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)

-j3-timeout

Provided by: J3 :: Provers configuration
Type: integer
Default: 2
Set a timeout in seconds for all the provers. Use 0 for no timeout.

-j3-verbose

Provided by: J3 :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in J3

-j3-z3-steps

Provided by: J3 :: Provers configuration
Type: integer
Default: 0
Set a steps limit for Z3. Use 0 for no steps limit.

-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-classpath

Provided by: Java
Type: string
Default: .
Specify where to find user class files.

-java-debug

Provided by: Java :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in Java

-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-main

Provided by: Java
Type: string
Default: <none>
Sets the entrypoint of the Java program.

-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-reflection

Provided by: Java
Type: boolean
Default: false
Opposite option: -no-java-reflection
Add reflection support for the Java plugin.

-java-runtime

Provided by: Java
Type: boolean
Default: false
Opposite option: -no-java-runtime
Adds runtime files for the Java plugin.

-java-share-literal-strings

Provided by: Java
Type: boolean
Default: true
Opposite option: -java-no-share-literal-strings
comply with JLS#3.10.5 rule stating a given string literal always refer to the same instance of the class java.lang.String.

-java-sourcepath

Provided by: Java
Type: string
Default: .
Specify where to find user source files. This is used by the GUI to display the source file along the normalized source code.

-java-translate-all-classes

Provided by: Java
Type: boolean
Default: false
Opposite option: -java-no-translate-all-classes
Force all classes to be translated.

-java-verbose

Provided by: Java :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in Java

-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, java
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

-license-debug

Provided by: License :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in License

-license-help

Provided by: License :: Getting Information
Type: boolean
Default: false
Opposite option: <none>
help of plug-in License

-license-msg-key

Provided by: License :: Output Messages
Type: set
Default: <none>
Categories: <none>
enables message display for categories <k1>,…,<kn>. Use -license-msg-key help to get a list of available categories, and * to enable all categories

-license-retry

Provided by: License
Type: integer
Default: <none>
Try <count> times to get a token if none is available. By default the analyzer stops immediately if no token is available.

-license-verbose

Provided by: License :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in License

-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.

-mcdc

Provided by: MC/DC coverage
Type: boolean
Default: false
Opposite option: -no-mcdc
Collect information to compute MC/DC coverage later on.

-mcdc-compute

Provided by: MC/DC coverage
Type: boolean
Default: false
Opposite option: -mcdc-no-compute
Compute decision coverage. Needs value analysis results (in interpreter mode) and also the results graph (obtainded with -whole-program-graph) to compute MC/DC on mixed conditions (see user documentation for more details). Only useful when having only one analysis, otherwise, tis-aggregate should be used.

-mcdc-debug

Provided by: MC/DC coverage :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in MC/DC coverage

-mcdc-help

Provided by: MC/DC coverage :: Getting Information
Type: boolean
Default: false
Opposite option: <none>
help of plug-in MC/DC coverage

-mcdc-msg-key

Provided by: MC/DC coverage :: Output Messages
Type: set
Default: <none>
Categories: <none>
enables message display for categories <k1>,…,<kn>. Use -mcdc-msg-key help to get a list of available categories, and * to enable all categories

-mcdc-verbose

Provided by: MC/DC coverage :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in MC/DC coverage

-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 expressed as address ranges. Named regions can be used when specifying address ranges in other options (see -absolute-address).

Regions are specified as a comma-separated list. Each region is defined by providing an arbitrary label and either a single address or a range of addresses.

A single address is expressed as a 64-bit integer in decimal, hexadecimal (‘0x’, ‘0X’), octal (‘0o’, ‘0O’), or binary (‘0b’, ‘0B’) notation, e.g.:
```
-memory-region=sensor:0x4080
```
A range can be expressed through its inclusive boundaries ‘[START_ADDR..END_ADDR]’ where ‘START_ADDR’ and ‘END_ADDR’ are precise addresses, e.g.:
```
-memory-region=input:[0x0x40a0..0x40af],output:[0x0x40b0..0x40bf]
```
A range can also be expressed by a start address and length ‘ADDR[LEN]’ where ADDR is a precise address and LEN is a 64-bit integer in decimal, hexadecimal (‘0x’, ‘0X’), octal (‘0o’, ‘0O’), or binary (‘0b’, ‘0B’) notation. E.g.:
```
-memory-region=page:0x8000[4096]
```
A range expressed as ‘[START_ADDR..END_ADDR]’ is equivalent to a range expressed as ‘STAR_ADDR[END_ADDR-START_ADDR-1]’.

Memory regions cannot include the address ‘0x0’.

See TrustInSoft User Guide on Dealing with special features (Physical addresses) for more information.

-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-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-annot-fct

Provided by: Kernel :: Parsing
Type: set
Default: <none>
Categories: <none>
ignore all the annotations of the given set of functions

-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

-override-static-fun

Provided by: Kernel
Type: list
Default: <none>
Replace all calls to a given static function by a given stub function.

-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-filter

Provided by: Kernel :: Input/Output Source Code
Type: set
Default: <none>
Categories: <none>
pretty print original code by keeping globals matching the given set of prefixes.

-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

Provided by: Kernel :: Customizing Normalization
Type: boolean
Default: false
Opposite option: -no-remove-volatile
Remove the ‘volatile’ qualifier from the type of all globals, locals, function declarations and function definitions.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-remove-volatile-locals

Provided by: Kernel :: Customizing Normalization
Type: set
Default: <none>
Categories: <none>
Remove the ‘volatile’ qualifier from all local variables defined within the specified set of functions.

The set of affected functions is expressed as a comma-separated list of function names, e.g.:
```
-remove-volatile-locals=main,f,g,h
```
See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-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 through 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-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: true
Opposite option: -no-strict-type-qualifier-merging
Strictly enforce type compatibility rules with respect to type qualifiers.

-stubgen-debug

Provided by: Stubgen :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in stubgen

-stubgen-header

Provided by: Stubgen
Type: string
Default: <none>
generate a default stub for all function declared in <header_file.h>

-stubgen-help

Provided by: Stubgen :: Getting Information
Type: boolean
Default: false
Opposite option: <none>
help of plug-in stubgen

-stubgen-msg-key

Provided by: Stubgen :: Output Messages
Type: set
Default: <none>
Categories: <none>
enables message display for categories <k1>,…,<kn>. Use -stubgen-msg-key help to get a list of available categories, and * to enable all categories

-stubgen-out

Provided by: Stubgen
Type: string
Default: <none>
output the generated stubs to <filename.c>

-stubgen-verbose

Provided by: Stubgen :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in stubgen

-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-fuzz-debug

Provided by: Tis-fuzz :: Output Messages
Type: integer
Default: 0
Possible values: integers >= 0
level of debug for plug-in tis-fuzz

-tis-fuzz-help

Provided by: Tis-fuzz :: Getting Information
Type: boolean
Default: false
Opposite option: <none>
help of plug-in tis-fuzz

-tis-fuzz-msg-key

Provided by: Tis-fuzz :: Output Messages
Type: set
Default: <none>
Categories: <none>
enables message display for categories <k1>,…,<kn>. Use -tis-fuzz-msg-key help to get a list of available categories, and * to enable all categories

-tis-fuzz-runtime

Provided by: Tis-fuzz
Type: boolean
Default: false
Opposite option: -tis-fuzz-no-runtime
Add ‘tis-fuzz’ runtime to the source files.

-tis-fuzz-share

Provided by: Tis-fuzz
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)

-tis-fuzz-verbose

Provided by: Tis-fuzz :: Output Messages
Type: integer
Default: 1
Possible values: integers >= 0
level of verbosity for plug-in tis-fuzz

-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-bin

Provided by: Server
Type: string
Default: <none>
specify the path of the tis-mkfs binary to use instead of relying on the PATH environment variable to find it.

-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-report

Provided by: Info :: Results
Type: boolean
Default: false
Opposite option: -no-tis-report
generate all files needed by tis-report in directory _results. This may be changed with the option -tis-report-directory

-tis-report-basename

Provided by: Info :: Results
Type: string
Default: <none>
generate tis-report files with names based on ‘basename’. Beware: ensure to set this option before the -tis-report option.

-tis-report-directory

Provided by: Info :: Results
Type: string
Default: _results
generate tis-report files to directory basedir. Beware: ensure to set this option before the -tis-report option.

-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 type checking 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_cosh:tis_cosh, __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_hypot:tis_hypot, __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_nextafter:tis_nextafter, __builtin_nextafterf:tis_nextafterf, __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_sinh:tis_sinh, __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_tanh:tis_tanh, __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, cosh:tis_cosh, exp:tis_exp, expf:tis_expf, floor:tis_floor, floorf:tis_floorf, fmax:tis_fmax, fmin:tis_fmin, fmod:tis_fmod, free:tis_free, hypot:tis_hypot, 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, nextafter:tis_nextafter, nextafterf:tis_nextafterf, pow:tis_pow, powf:tis_powf, printf:tis_printf, realloc:tis_realloc, round:tis_round, roundf:tis_roundf, sin:tis_sin, sinh:tis_sinh, 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, tanh:tis_tanh, 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 (uninitialized or containing escaping address). Any number of functions 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: pointer
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
Build a new project (named “Volatile”) where volatile access are simulated by function calls.

Functions simulating accesses to specific volatile variables are declared through code annotations or via automatic binding.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-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>
Treat a set of global variables or absolute addresses as if they were volatile. The analyzer assumes volatile variables can potentially be modified externally to the analyzed program at any point in its execution.

The option accepts a commma separated list of global variables found in the program, e.g.:
```
-volatile-globals=sensor,port,shared
```
The option can also be set to ‘NULL’, at which point the entire range of valid absolute addresses (see -absolute-valid-range) is treated as volatile, e.g.:
```
-volatile-globals=NULL -absolute-valid-range=0x4000-0x8000
```
See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-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
Print 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
Warn if a variable with the ‘volatile’ qualifier does not provide functions to simulate either reads or writes, but is either read from or written to anyway. Used in conjunction with -volatile.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-warning-on-volatile-casts

Provided by: Volatile
Type: boolean
Default: true
Opposite option: -no-warning-on-volatile-casts
Warn on casts which may loose the ‘volatile’ qualifier. Used in conjunction with -volatile.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-warning-on-volatile-lvalues

Provided by: Volatile
Type: boolean
Default: true
Opposite option: -no-warning-on-volatile-lvalues
Warn if a variable with the ‘volatile’ qualifier does not provide functions to simulate accesses, but is accessed anyway. Used in conjunction with -volatile.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-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-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
Model volatile access to be sound.

Use -wp-no-volatile to ignore volatile attributes.

See TrustInSoft User Guide on Dealing with special features (Volatile variables) for more information.

-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.