`tis-info` Manual¶

Introduction¶

This plug-in extracts a lot of useful information from the current project.

The information about each element is printed on a single line comma separated fields, which means that the result can be saved as a .csv file.

Theses files can be opened in a spreadsheet tool for easy selection. Moreover, it makes it easy to select some of them with grep. And if you are familiar with SQL, you can even build a sqlite database to make more elaborate requests over several .csv files (see tis-aggregate sql-export).

To generate all the .csv files from a project, use the -info-csv-all option.

Some pieces of information are syntactic, and some others are semantic and are only available when the project holds value analysis results.

About Functions¶

When the -info-functions options is used, some information is printed for each function of the current project.

The following list explains which information can be found in each column:

Function: internal function name.

UserName: user function name.

Is defined: tells whether the function has a body or if it is an external function. The possible values are:

defined: if the function has a defined body

undefined: if the function is external

Is static: tells whether the function is static or has a global scope. The possible values are:

static: if the function is static

global: if the function has a global scope

Addr used: tells whether the address of the function is used. The possible values are:

yes

no

Is called: tells if the function is syntactically called somewhere in the application. Notice that the entry point (main function) is considered as called. The possible values are:

called: if the function is syntactically called

not called: otherwise

Is reachable: tells if the function is semantically reachable from the entry point. Notice that this information is only available if the project contains value analysis results. The possible values are:

NA: if no value analysis results are available

reachable: if the function has been reached during analysis

unreachable: otherwise

Aliases: tells whether the function is aliased to other function declarations from the original source that may have disappeared from the merged file.

Clone origin: name of the source function if the function is a clone, ‘NA’ otherwise.

Spec: tells if the function has an ACSL specification. The possible values are:

user: if the user gave a specification

generated: if there is no user specification, but a specification has been generated by the tool

none: otherwise

This information is mainly interesting for undefined functions.

val-use: tells how the function is considered by the analyses. The possible values are:

built-in: if a built-in is used for this function, or if it is a built-in function

specification: if the function is not defined or if -val-use-spec options is used to cut the analysis on this function

body: otherwise

File: gives the file in which the function is defined (or declared).

Starting line: line of the file where the function begins. The values are integers.

Ending line: line of the file where the function ends. The values are integers.

#reached: tells how many statements of the function are semantically reachable. Notice that this information is only available if the project contains value analysis results to provide reachable information. The values are integers, where -1 means not available.

#total: gives the number of statements of the function. The values are integers.

coverage: gives the coverage percentage if the reachable information is available. The value is NA otherwise.

#called: represents how many times this function has been called during the analysis. The values are integers, where -1 means not available.

Overhead time: represents the time spent analyzing a function minus the time spent analyzing its statements or the associated built-in (expressed in seconds). The values are floating point numbers or 0.0 when not available.

Self time: represents the time spent analyzing a function minus the time spent analyzing its call statements (expressed in seconds). The values are floating point numbers or 0.0 when not available.

Total time: represents the time spent analyzing a function (expressed in seconds). The values are floating point numbers or 0.0 when not available.

Memexec time: time taken by memexec to check if we can reuse a previous call and to store a new call (expressed in seconds). The values are floating point numbers or 0.0 when not available.

Memexec hits: represents how many time previous analysis results of this function have been reused by memexec. The values are integers, where -1 means not available.

Is libc: tells whether the function is provided by the standard C library. The possible values are:

libc:no

libc:yes

Reached stdlib: similar to ‘Is libc’, but also tells whether the function is reachable. The possible values are:

No: if it is not an stdlib function

Used: if it is an stdlib function that is called

Yes: if it is an stdlib function

Cyclomatic complexity: McCabe’s cyclomatic complexity The values are integers.

The -info-csv-functions filename option export the same information into the given filename.

About Statements¶

When the -info-statements options is used, some information is printed for each statement of the current project.

The following list explains which information can be found in each column:

Sid: internal unique statement identifier. The values are integers.

File: file where the statement is.

Line: line of the file where the statement is. The values are integers.

Function: name of the enclosing function.

Number: statement number inside the function. This is the number used when printing REACHED information. The values are integers.

Reachable: tells if the statement is reachable. Notice that this information is only available if the project contains value analysis results. The possible values are:

NA: if no value analysis results are available

reachable: if the statement has been reached during analysis

unreachable: otherwise

never-terminating: if the value analysis of this statement never terminated

non-terminating: if the value analysis of this statement did not terminate for some paths

unpropagated: if the results for that statement are incomplete due to a value analysis degeneration

degenerated: if the value analysis has degenerated here

Dead code entry: flag the statements that are dead code entry points. A dead code entry point is a dead statement that, either it has no predecessor (it is the first statement of an unreachable function, or it is syntactically an unreachable statement) or it has at least one reachable predecessor. The possible values are:

yes

no

Notice that this information is only available if the project contains value analysis results, otherwise no statement is flagged.

Dead code exit: flag the statements that are dead code exit points. A dead code exit point is a dead statement that, either it has no successor (it is the last statement of an unreachable function for instance) or it has at least one reachable successor. The possible values are:

yes

no

Notice that this information is only available if the project contains value analysis results, otherwise no statement is flagged.

Dead Id: give a unique id per function for each contiguous statement/block not reachable by the Value Analysis (with an exception for values 0 and -1). If the Value Analysis results are not available, all dead ids are set to -1. It allows to unambiguously refer to pieces of dead code in functions. If the function is not reachable at all by the Value Analysis, then all dead ids of this function statements are 0. If a statement is reachable by the Value Analysis, its dead ids is -1.

Kind: kind of the statement. The possible values are:

test: a test (if). See next column for more information

function call: a function call. See next column for more information

instruction: a simple instruction, such as an assignment for instance

inline assembly: for assembly statements

loop

return

jump: for statements like goto, break, continue

switch

block

unspecified sequence: for a sequence of instructions that comes from the decomposition of an instruction of the original program, and for which the order of evaluation in unspecified.

other statement

More: gives more information on the statement depending on its kind. The possible values are:

(else branch dead | then branch dead | no reduction): for a test, when the reachability has been computed, indicates if one of the two branches is alive and the other one is dead. Moreover, if the -info-stmt-no-reduction option is used, and both branches are alive, and the results are available, indicates whether the states are the same in both branches, which means that the effect of the conditional has definitely been over-approximated. Nothing is printed otherwise.

direct call: for a direct call

indirect call: for an indirect call, and gives moreover:

the list possibly indirectly called functions if available,

NA otherwise (that is: indirect but not analyzed).

loop n°%d in the function: loop number in the function. This information is useful when importing ACSL loop properties for instance

Join reason: represents why the analysis joined several propagated states. The possible values are:

<none>: when no joins occurred on this statement

slevel merge: when slevel merge annotation is specified

merged loop: when a loop iteration analysis starts or ends with more than one propagated state (to disable this behavior, use -val-slevel-merge-after-loop=-@all)

reached slevel: when the slevel for this statement has been reached

widened: when the analyzer started to over approximate a loop (should only happen when the slevel is reached for the loop)

Notice that several value may be used for one statement.

SlevelCounter: is the maximum slevel reached for this statement for all calls. In other words, it represents how many separated states went through this statement. This is an over-approximation and gets cut once it reached the slevel. The values are integers, where -1 means not available. Notice that this information is only available if the project contains value analysis results.

SlevelLimit: is the statement slevel limit. The values are integers, where -1 means not available. Notice that this information is only available if the project contains value analysis results.

Slevel ratio: is (counter * 100 / slevel). The values are integers, where -1 means not available. Notice that this information is only available if the project contains value analysis results.

Widening: represents how many widening states went through this statement. There may be more than one widening state if we are in a loop and we do not find the fixpoint with the first widening iteration. The values are integers, where -1 means not available. Notice that this information is only available if the project contains value analysis results.

Self time: is the time spent analyzing this statement excluding potential calls. The values are floating point numbers or 0.0 when not available.

Self time: is the time spent analyzing this statement including potential calls. The values are floating point numbers or 0.0 when not available.

Is libc: tells whether the statement is provided by the standard C library. The possible values are:

libc:no

libc:yes

The -info-csv-statements filename option export the same information into the given filename.

About Files¶

When the -info-files options is used, some information is printed for each files of the current project.

The following list explains which information can be found in each column:

File: filename name.

#functions: number of function defined in this file. The values are integers.

Toplevel: tells whether the file is a toplevel one or if it has been included in another one. The possible values are:

yes: if the file a is toplevel one

no: if the file is not a toplevel one, i.e. it has been included in another one

maybe: if a preprocessed file has been provided to the analyzer, and the file has the same basename, it can probably be a toplevel file.

Is libc: tells whether the file is from the tool libc or not. The possible values are:

no

yes

The -info-csv-files filename option export the same information into the given filename.

About Types¶

When the -info-types options is used, some information is printed for each type of the current project.

Notice that the unused types are not listed since they are automatically removed from the internal representation.

The following list explains which information can be found in each column:

File: gives the file of the type definition/declaration.

Line: gives the line of the type definition/declaration.

Kind: gives the type kind. The possible values are:

typedef

enum

struct

union

Source name: gives the name found in the source file of the type for typedef, or of the tag otherwise. Print <empty> when the tag not specified.

Internal name: gives the internal name if different from the source name. The value is <same> otherwise.

Defined: tells whether the enum/struct/union is defined, or only declared. For typedef, tells whether the underlying type is abstract (top only). The possible values are:

defined

declared

Sub-type: meaningful for ‘typedef’ only: show the underlying type. The value is N/A otherwise.

Size (#bytes): gives the size of the type, in bytes, when available. The values are integers, where -1 means not available.

Is libc: tells whether the type is provided by the standard C library. The possible values are:

libc:no

libc:yes

The -info-csv-types filename option export the same information into the given filename.

About Variables¶

When the -info-variables options is used, some information is printed for each variable of the current project.

Notice that function variables are not listed here.

The following list explains which information can be found in each column:

Name(s): gives the name of the variable. Also give the internal name if the variable has been renamed to avoid ambiguities.

File: gives the file of the variable definition/declaration. The value is no valid location otherwise.

Line: gives the line of the variable definition/declaration.

Type: gives the type kind of the variable (sub-type are not developed).

Function: gives the function of the variable if any. The value is NA otherwise.

Kind: gives the kind of the variable. The possible values are:

global variable

local variable

formal variable: for function formal parameters

Warning: static local variables are marked as ‘global’ here.

Storage: tells if the variable is defined or just declared, and also if it is a static variable. The possible values are:

static

declared: only global variables might be only declared

defined

Initialized: tells whether the variable has an initializer or not. The possible values are:

no

yes

Notice that this is only meaningful for global variables since local initialization are transformed into statements.

Volatile: tells whether the variable is volatile or not. The possible values are:

no

yes

Notice that the qualification is detected anywhere in the type.

Const: tells whether the variable is const or not. The possible values are:

no

yes

Temporary: tells whether the variable is a temporary variables generated by the tool or a variables coming directly from user input. The possible values are:

no

yes

Is libc: tells whether the variable is provided by the standard C library. The possible values are:

libc:no

libc:yes

The -info-csv-variables filename option export the same information into the given filename.

About Shared Variables¶

When the -info-shared-variables options is used, some information is printed for each shared variable of the current project.

This table shows the access to the shared variables for each of the threads. It is only available after a Mthread analysis.

The following list explains which information can be found in each column:

Variable name: name of the shared variable.

File: file where the access takes place.

Line: line of the file where the access takes place.

Access kind: access kind. The possible values are:

write: when the variable may be written by this statement.

read: when the variable is only read.

Thread: name of the thread that does the access.

Function: function where the access takes place.

Statement number: statement number inside the function. The values are integers.

Protecting Mutexes: list of the mutex and their locking status where true means the mutex is locked and false means it may be locked or not.

The -info-csv-shared-variables filename option export the same information into the given filename.

About Properties¶

When the -info-properties options is used, some information is printed for each property of the current project.

The following list explains which information can be found in each column:

File: tells the location file of:

the statement of the property for a local annotation,

the statement of the call for an instance of a precondition,

the function for a function contract property,

the property itself otherwise.

Line: gives the line in the file

Function: gives the name of the function in which the property is if any. The value is NA otherwise.

StmtId: for local properties, gives the number of the statement in the function. The values are integers, where -1 means not available.

Kind: gives the kind of property. The possible values are:

differing blocks

division by zero

float to int

index out of bound

invalid shift

is NaN or infinite

logic memory access

memory access

not separated

overflow

overlap

pointer comparison

pointer equality

uninitialized

valid string

valid wstring

comparable char blocks

comparable wchar blocks

dangling contents

division overflow

function pointer

index in address

pointer arithmetic

unclassified

bad libc call

UB assert

UB precondition

assert

loop invariant

invariant

requires

assumes

ensures

exits

breaks

continues

returns

terminates

allocates

assigns

behavior: not really a property but rather a collection of properties (see ACSL manual)

complete behaviors

decrease

disjoint behaviors

from

axiom

axiomatic: not really a property but rather a collection of properties (see ACSL manual)

lemma

instance of requires: for instances of requires properties at the call statements

reachability: for properties about the reachability of functions and statements

other: for other properties

Name: gives the name of the property if any. The value is <empty string> otherwise. When adding properties, it is very recommended to give them names to easily identify them.

Status: gives the verification status of the property. The possible values are:

surely valid: the status is True and the dependencies have the consolidated status
surely_valid or considered_valid.

considered valid: there is no possible way to prove the property (e.g., the post-condition of an external function). We assume this property will be validated by external means.

valid under hypothesis: the local status is True but at least one of the dependencies has a consolidated status unknown. This is typical of proofs in progress.

valid but dead: the status is True, but the property is in a dead or incoherent branch.

unknown: the status is Maybe.

unknown but dead: the local status is Maybe, but the property is in a dead or incoherent branch.

surely invalid: the status is False,
and the dependencies the consolidated have status surely_valid.

invalid under hypothesis: when the local status is False,
but at least one of the dependencies has status unknown. This is a sign of a dead code property, or of an erroneous annotation.

invalid but dead: the local status is False,
but the property is in a dead or incoherent branch.

inconsistent: there exists two conflicting consolidated statuses for the same property, for instance with values surely_valid and surely_invalid. This case may also arise when an invalid cyclic proof is detected. This is symptomatic of an incoherent axiomatization.

never tried: no status is available for the property.

See the user manual for more information about the status.

Alarm: tells whether the property is a generated alarm or not. The possible values are:

yes

no

Alarm rank: gives the rank of the emitted alarm if the property is a Value analysis alarm. The values are integers, where -1 means not available. It is advisable to study the alarms in the order in which they have been emitted since an alarm may alter the states after it.

MoreInfo: gives some more information about the property. Deprecated: rather use other tables to get more information. The possible values are:

global

in unreachable function: similar to _but_dead status suffix.

inside -val-use-spec function: annotation are not reached in use-spec functions.

ensures of -val-use-spec function: post-condition of use-spec functions cannot be checked, they are used as hypotheses.

at unreachable statement: local annotation attached to an unreachable statement.

instance of builtin requires: instance of a built-in pre-condition can be safely ignored since the built-in raises alarms in cas of problems.

<empty string>: No additional information

Is libc: tells whether the property is provided by the standard C library. The possible values are:

libc:no

libc:yes

The -info-csv-properties filename option export the same information into the given filename.

Examples¶

Let’s examine project_properties.csv:

On a project with value analysis results, it could be interesting to find the unreachable properties that are not part of the library with:
```
$ grep never_tried project_properties.csv | grep -v TIS_KERNEL_SHARE
```
To find invalid properties:
```
$ grep invalid project_properties.csv
```
To find all the alarms generated by Value, sorted by their kind:
```
$  grep -v 'alarm:(no|NA)' project_properties.csv |  sort -k5
```

To find the unverified user properties, sorted by function name:

$ cat project_properties.csv | grep 'alarm:(no|NA)' | grep -v ', valid,' \
       | grep -v 'TIS_KERNEL_SHARE.*never_tried' | sort -k2

About Value analysis results¶

The -info-results option may be used to print some information about the result of a value analysis. The default is to print all the sections, but a selection can be done by using the -info-msg-key results:xxx option. To know all the possible values for xxx, run:

$ tis-analyzer -info-msg-key help

There is no option at the moment to print all the sections except some of them, but because each line is prefixed with its category, it is quite easy to filter out some of them. For instance:

$ tis-analyzer ... -info-results \
  | grep "^\[info:results" | grep -v "info:results:coverage"

Some -info-results-skip-xxx options are provided as well to specify elements that may be skipped in the report. For instance -info-results-skip-abort e1,..en specifies the functions that are known to exit (they do not terminate) and that do not need to be reported as elements to check. The specified expressions e may be simple function names, but also regular expressions.

The other -info-results-skip-xxx options work similarly. All of them may take a list or may be used several times on the command line. See the All Options section for more information.

The -info-json-results option may provide an output file name to which the results are exported using the JSON format presented below.

Errors¶

The result sections presented below, that are marked with a VERIF_ERROR tag in the results, are the most important one. All the problems listed in these sections must be solved before going further.

Section `results:undef`¶

This section reports the existence of some reachable functions with neither code nor specification.

This MUST be fixed either by providing source files with the body of these functions, or by adding them some specifications (with at least ‘assigns’ properties). When functions are listed in this section, the obtained results are probably meaningless.

Section `results:degeneration`¶

The degeneration are points where the value analysis stopped. Results are not correct for lines of code that can be reached from the degeneration point, so this MUST be fixed.

Section `results:non-terminating`¶

This section reports the other non-terminating statements.

Some abort like functions may appear here: this is normal. The application functions which are known to never terminate may be excluded using the -info-results-skip-abort option. Other cases must be examined carefully.

Section `results:messages`¶

This section reports some messages from the tool.

Some of them are purely informative, but all of them have to be carefully reviewed manually.

Section `results:alarms`¶

This section reports the generated alarms.

The alarms should be reviewed carefully, and removed if possible. Starting from the first one is a good idea, since the next ones may be due to related reasons.

More things to examine¶

The following sections do not report errors per se, but pieces of information that should be checked to see if everything seems normal about them.

Section `results:hypotheses`¶

This section lists the hypotheses to verify.

Beside the alarms, these properties must be proved or justified. Some of them may be proved with WP, or manually justified. If named carefully (as explained in Naming the Annotations) - for instance with wp and rv - you can exclude them from this list using the -info-results-skip-props _wp,_rv.

Section `results:no-body-but-spec`¶

This section lists the functions with no code, but specifications.

These should be library functions. Some of them may be ignored by using the -info-results-skip-lib option. The specified expression may also match the filename. For instance, with -info-results-skip-lib external_headers all the function from file in the external_headers directory are ignored.

Section `results:body-but-use-spec`¶

This section lists the functions with code, but which are nevertheless analyzed using their specification only.

These functions have a body, but the value analysis has been asked to ignore them and to use their specifications instead (with the -val-use-spec option). They are listed here as a remainder that the analysis has been done under these hypotheses, and that at the end, these specifications MUST be checked by analyzing these functions alone.

Section `results:builtins`¶

This section lists the functions from tis-analyzer libc and built-ins that have been used. These functions that come from the tool are only listed here to show which ones are used.

Section `results:useless-files`¶

This section lists the source files that contain no reachable functions.

In most cases these files can be safely removed from the analysis, unless they hold the definition (and the initialization) of a used global variable. It is harmless to keep them though, and it can even be useful for measuring the coverage over the whole application.

Some more information¶

The following sections provide more information that can be interesting to look at.

Section `results:coverage`¶

This section gives an overview of the analysis coverage.

This information may be interesting to analyze at the end of the study, but can be skipped during the elaboration of the analysis when these numbers can change a lot, which can be annoying.

To examine more precisely the coverage (by function), rather use the tis-aggregate coverage command (see tis-aggregate coverage).

Section `results:precision`¶

The -info-precision option is used to specify the level of information printed about the loss of precision during the analysis. This option takes an integer which may be:

0: no information (default level),
1: a summary gives the number of statements and loops where precision has been lost,
2: the information is given on each statement where precision has been lost,
3: 2 + the statement itself is also printed.

For a positive level, it sets -info-msg-key results:precision, and if -info-msg-key results:precision is set and the precision level is not specified, it is set to 1.

Precision may be lost when:

the specified slevel is reached (see -slevel option documentation),
states are merged in a loop (see -val-slevel-merge-after-loop option documentation),
a widening has been done in a loop (see -wlevel option documentation).

Section `results:exits`¶

This section shows information about the exit status of the analyzed application. It provides:

the reachability of the entry point return statement,
the value returned by the entry point (if any),
the number of exit calls reached during the analysis,
the value of the status used by exit calls (if any).

You could also be interested by the Termination information on statements to know if some more non-terminating statements can be reached.

JSON format¶

The file generated when using the -info-json-results option holds the same information that are presented above and respect the following format.

Warning

This is an experimental feature, and the format might change a little in the next release.

computation (progress of preparing and computing the value analysis)
- type: string = error (must be solved before going further)
- status: string, one of {OK, NOT OK} (NOT OK if a problem blocking the analysis or making its results inaccessible has been encountered, OK otherwise)
  - if NOT OK then the error field must be present
- error: optional string, one of:
  - no input file
  - config error
  - pre-action failed (a required action before the parsing has failed)
  - parsing error
  - missing file
  - link error
  - no value analysis computation (the value analysis was not demanded, thus it was not computed at all)
  - no entry point
  - incorrect number of arguments
  - invalid user input
  - unexpected error
- message: optional string (more information about the encountered problem, if available)
  - when error is config error or missing file, message always holds the name of the concerned file
  - when error is parsing error, message holds information about the parsing error that occurred with its location
  - when error is no entry point, message always holds the name of the expected entry point
  - when error is no input file, incorrect number of arguments, no value analysis computation, or no value analysis results, there is no message field
  - when error is link error or `unexpected error, message is optional; if present, it holds some additional information about the error
undefined_functions (reachable functions with neither code nor specification)
- type: string = error (must be solved before going further)
- status: string, one of {OK, NOT OK} (NOT OK if any reachable function with neither code no specifications has been encountered, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of objects (locations of the declarations of each reachable undefined function):
  - file: string (path to the file)
  - line: integer (line number in the file)
  - function: string (name of the function)
degeneration (point in the program where the value analysis stopped)
- type: string = error (must be solved before going further)
- status: string, one of {OK, NOT OK} (NOT OK if a degeneration has occurred, OK otherwise)
  - if NOT OK then the reason field must be present
- reason: optional string (degeneration reason), one of:
  - user interruption
  - timeout
  - out of memory
  - stop at nth alarm
  - stop at nth garbled
  - stop at first tis check included
  - entry point with unexpected args
  - pointer library function
  - throwing library function
  - recursive call
  - recursive clone depth has reached the limit
  - writing at unknown address
  - assign with extern function
  - fail to call builtin
  - invalid call to builtin
  - cannot resolve format string
  - format string not supported
  - watchpoint
  - interpreter not a singleton
  - interpreter invalid property
  - interpreter format string percent p
  - interpreter assign in extern function
  - interpreter encounters a limitation
- additional fields depending on reason
  - when reason is invalid call to builtin or entry point with unexpected args: or interpreter invalid property:
    - message: string (more information about the problem)
  - when reason is format string not supported:
    - may_be_invalid: boolean
  - when reason is interpreter not a singleton:
    - expression: string (the expression that cannot be evaluated to a single value)
    - imprecision: array of one object among:
      - variable: object:
        
        name: string (name of the variable involved in the expression)
        
        type: string (type of the variable)
        
        volatile: boolean
        
        undefined: boolean
      - volatile_lvalue: string (volatile sub-expression)
      - imprecise_lvalue: string (imprecise sub-expression)
      - imprecise_pointed_value: object:
        
        pointer: string (pointer expression)
        
        pointer_type: string (type of the pointer)
        
        pointer_value: string (pointed expression)
      - imprecise_operation: object:
        
        expression: string (imprecise expression)
        
        type: string (type of the expression)
        
        value: string (value of the expression)
        
        sub-expressions: array of objects:
        
        expression: string (sub-expression)
        
        type: string (type of the sub-expression)
        
        value: string (value of the sub-expression)
- program_point optional object (point in the program where the degeneration occurred)
  - file: string (path to the file)
  - line: integer (line number in the file)
  - function: string (name of the function)
  - function_start_line: integer (the line number where function begins in file)
  - function_end_line: integer (the line number where function ends in file)
  - statement_kind: string, one of:
    - test
    - function call
    - instruction
    - inline assembly
    - loop
    - return
    - jump
    - switch
    - block
    - unspecified sequence
    - other statement
  - additional fields depending on statement_kind (similar to the More column of info-statements):
    - when statement_kind is loop:
      - loop_number: integer (number of the loop in the function)
    - when statement_kind is function call:
      - direct_call: boolean (is the call direct or indirect)
      - when direct_call is true:
        
        called_function: string (name of the function which is called directly)
      - when direct_call is false:
        
        called_functions: array of strings (names of functions which may be called indirectly), may be empty if the call is not reachable or if the value of the pointer is not available
non_terminating (other non-terminating statements)
- type: string = to verify (not an error, but needs to be checked)
- status: string, one of {OK, NOT OK} (NOT OK if any non-terminating statement has been encountered, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- skipped: optional array of strings (names of functions specified using the -info-results-skip-abort option, known to not terminate and thus ignored here; these functions have been excluded from the list array below)
- list: optional array of objects (details of each non-terminating statement):
  - never_terminating: boolean (true if the statement never terminates, false if it may terminate for some callstacks)
  - program_point object (point in the program where the non-terminating statement is located)
    - file: string (path to the file)
    - line: integer (line number in the file)
    - function: string (name of the function)
    - function_start_line: integer (the line number where function begins in file)
    - function_end_line: integer (the line number where function ends in file)
    - statement_kind: string, one of:
      - test
      - function call
      - instruction
      - inline assembly
      - loop
      - return
      - jump
      - switch
      - block
      - unspecified sequence
      - other statement
    - additional fields depending on statement_kind (similar to the More column of info-statements):
      - when statement_kind is loop:
        
        loop_number: integer (number of the loop in the function)
      - when statement_kind is function call:
        
        direct_call: boolean (is the call direct or indirect)
        
        when direct_call is true:
        
        called_function: string (name of the function which is called directly)
        
        when direct_call is false:
        
        called_functions: array of strings (names of functions which may be called indirectly), may be empty if the call is not reachable or if the value of the pointer is not available
    - call_stacks: optional array of array of objects (list of call stacks; each call stack is described by list of objects representing the call sites). A call site has the following fields:
      - function: string (function of the call site)
      - file: string (file of the call site)
      - line: integer (line in file of the call site)
      Note: an empty array means the program point is located in the entry point of the program.
messages (selected log file messages)
- type: string = to verify (not an error, but needs to be checked)
- status: string, one of {OK, NOT OK} (NOT OK if some important messages have been emitted such as warnings or errors, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- skipped: optional array of strings (messages specified using the -info-results-skip-log option, known to be normal and thus ignored here; messages matching these regular expressions and messages concerning plugins with names matching these regular expressions have been excluded from the list array below)
- list: optional array of objects (details of each message):
  - message: string (text of the message)
  - plugin: string (name of the plugin that emitted the message)
  - kind: string, one of:
    - warning
    - user error
    - failure
  - location: optional object (location of the problem in the source file if any)
    - file: string (path to the file)
    - line: integer (line number in the file)
alarms (generated alarms)
- type: string = error (must be solved before going further)
- status: string, one of {OK, NOT OK} (NOT OK if any alarm has been generated, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of objects (details of each generated alarm):
  - kind: string, one of:
    - differing blocks
    - division by zero
    - float to int
    - index out of bound
    - invalid shift
    - is NaN or infinite
    - logic memory access
    - memory access
    - not separated
    - overflow
    - overlap
    - pointer comparison
    - pointer equality
    - uninitialized
    - valid string
    - valid wstring
    - comparable char blocks
    - comparable wchar blocks
    - dangling contents
    - division overflow
    - function pointer
    - index in address
    - pointer arithmetic
    - unclassified
    - bad libc call
    - UB assert
    - UB precondition
  - additional fields depending on kind
    - when kind is unclassified:
      - description: string (description of the alarm)
    - when kind is not unclassified:
      - predicate: string (alarm ACSL predicate)
    - when kind is unclassified``or ``function pointer:
      - details: optional string (details about the alarm when available)
  - rank: optional integer (emission rank of the alarm when it is emitted by the value analysis)
  - status: string (status of the property), one of:
    - surely valid
    - considered valid
    - valid under hypothesis
    - valid but dead
    - unknown
    - unknown but dead
    - surely invalid
    - invalid under hypothesis
    - invalid but dead
    - inconsistent
    - never tried
  - program_point object (point in the program where the alarm has been generated)
    - file: string (path to the file)
    - line: integer (line number in the file)
    - function: string (name of the function)
    - function_start_line: integer (the line number where function begins in file)
    - function_end_line: integer (the line number where function ends in file)
    - statement_kind: string, one of:
      - test
      - function call
      - instruction
      - inline assembly
      - loop
      - return
      - jump
      - switch
      - block
      - unspecified sequence
      - other statement
    - additional fields depending on statement_kind (similar to the More column of info-statements):
      - when statement_kind is loop:
        
        loop_number: integer (number of the loop in the function)
      - when statement_kind is function call:
        
        direct_call: boolean (is the call direct or indirect)
        
        when direct_call is true:
        
        called_function: string (name of the function which is called directly)
        
        when direct_call is false:
        
        called_functions: array of strings (names of functions which may be called indirectly), may be empty if the call is not reachable or if the value of the pointer is not available
    - call_stacks: optional array of array of objects (list of call stacks; each call stack is described by list of objects representing the call sites). A call site has the following fields:
      - function: string (function of the call site)
      - file: string (file of the call site)
      - line: integer (line in file of the call site)
      Note: an empty array means the program point is located in the entry point of the program.
  - values: optional array of objects:
    - lvalue: lvalue that appears in the predicate
    - values: possible values of the lvalue
hypotheses (hypotheses to verify)
- type: string = to verify (not an error, but needs to be checked)
- status: string, one of {OK, NOT OK} (NOT OK if there are some hypotheses to verify, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- skipped: optional array of strings (names of properties specified using the -info-results-skip-props option, known to be verified elsewhere and thus ignored here; properties with matching substrings have been excluded from the list array below)
- list: optional array of objects (details of each property which has been used as a hypothesis):
  - kind: string, one of:
    - assert
    - loop invariant
    - invariant
    - ensures
    - exits
    - breaks
    - continues
    - returns
    - terminates
    - allocates
    - assigns
    - complete behaviors
    - decrease
    - disjoint behaviors
    - from
    - axiom
    - axiomatic
    - lemma
    - instance of requires
    - other
  - name: optional string (name of the property, if any)
  - status: string (status of the property), one of:
    - surely valid
    - considered valid
    - valid under hypothesis
    - valid but dead
    - unknown
    - unknown but dead
    - surely invalid
    - invalid under hypothesis
    - invalid but dead
    - inconsistent
    - never tried
  - more_information: optional string, one of:
    - global
    - in unreachable function
    - inside -val-use-spec function
    - ensures of -val-use-spec function
    - at unreachable statement
    - instance of builtin requires
    - empty string
  - file: string (path to the file)
  - line: integer (line number in the file)
  - function: optional string (name of the function)
no_body_but_spec (functions with no code, but with specifications)
- type: string = to verify (not an error, but needs to be checked)
- status: string, one of {OK, NOT OK} (NOT OK if any function with no body but with specifications has been encountered, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- skipped: optional array of strings (names of functions specified using the -info-results-skip-lib option, known to be library functions and thus ignored here; these functions have been excluded from the list array below)
- list: optional array of strings (names of functions)
body_but_use_spec (functions with bodies, but which are analyzed using their specifications only)
- type: string = informative (information that may be interesting to look at)
- status: string, one of {OK, NOT OK} (NOT OK if any function which has a body has been analyzed using its specifications only, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of strings (names of functions)
external_variables (used external variables)
- type: string = informative (information that may be interesting to look at)
- status: string, one of {OK, NOT OK} (NOT OK if the value of any undefined (i.e. declared external global) variable has been used, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of objects (used external variables with their declaration location):
  - name: string (name of the variable)
  - type: string (type of the variable)
  - file: string (path to the file)
  - line: integer (line number in the file)
assembly (reachable assembly statements)
- type: string = informative (information that may be interesting to look at)
- status: string, one of {OK, NOT OK} (NOT OK if any reachable assembly statements has been encountered, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of objects (locations of the assembly statements):
  - file: string (path to the file)
  - line: integer (line number in the file)
  - function: string (name of the function)
builtins (used functions from the tis-analyzer libc and built-ins)
- type: string = informative (information that may be interesting to look at)
- status: string, one of {OK, NOT OK} (NOT OK if any function from the tis-analyzer libc or a built-in has been used, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of strings (names of functions or built-ins)
useless_files (source files that contain no reachable functions)
- type: string = to verify (not an error, but needs to be checked)
- status: string, one of {OK, NOT OK} (NOT OK if any source file containing no reachable functions has been encountered, OK otherwise)
  - if NOT OK then the list field must be present and not empty
- list: optional array of strings (names of useless files)
coverage (overview of the analysis coverage)
- type: string = informative (information that may be interesting to look at)
- function_coverage: string, format X% (percentage of reachable functions)
- total_statements_coverage: string, format X% (percentage of reachable statements)
- semantic_statements_coverage: string, format X% (percentage of reachable statements in the reachable functions)
input_perimeter (Input values for the functions specified with the option -fun-inout)
- type: string = informative (information that may be interesting to look at)
- Function: string (name of the function)
- Call_stack: string (callstack up to the function call)
- Inputs: list of string (values of the operational inputs of the function)
precision (information about the loss of precision during the analysis and its reasons, and also about the value of some level counters)
- type: string = informative (information that may be interesting to look at)
- status: string, one of {OK, NOT OK} (NOT OK if any precision has been lost, OK otherwise)
  - if NOT OK then at least one of the reaching_slevel_stmts, reaching_malloc_plevel_stmts, widened_loops, or merged_loops fields must be present
- max_slevel: non-negative integer (maximum slevel that has been reached)
- max_malloc_plevel: optional positive integer (maximum malloc-plevel that has been reached if any)
- max_clone_depth: optional positive integer (maximum depth of the cloned recursive functions if any)
- reaching_slevel_stmts: optional positive integer (number of statements where the slevel has been reached)
- reaching_malloc_plevel_stmts: optional positive integer (number of statements where the malloc-plevel has been reached)
- widened_loops: optional positive integer (number of loops where a widening has been performed)
- merged_loops: optional positive integer (number of loops where states were merged)
time (optional information about the time taken by the analyzer. Available only if the -time option is set.)
- type: string = informative (information that may be interesting to look at)
- parsing_time: string representation of a positive float (time taken by the parsing in seconds)
- cxx_parsing_time: optional string representation of a positive float (time taken by the C++ parsing in seconds)
- java_parsing_time: optional string representation of a positive float (time taken by the Java parsing in seconds)
- value_analysis_time: string representation of a positive float (time taken by the parsing in seconds)
- total_time: string representation of a positive float (total time in seconds)
target (environment of the analysis: target machine, analysis entry point, program arguments)
- type: string = informative (information that may be interesting to look at)
- entry_point: string (name of the entry point function)
- entry_point_function: object (name and location of the entry point function): - file: string (path to the file) - function: string (name of the function) - function_start_line: integer (the line number where function begins in file) - function_end_line: integer (the line number where function ends in file)
- arguments: optional string (arguments given to the entry point with the -val-args option, if any)
- architecture: string (target architecture, corresponding to machdep)
- endianness: string, either little endian or big endian
entry_point_return: (information about the return value of the entry point function)
- type: string = informative (information that may be interesting to look at)
- reachable: boolean (reachability of the entry point function’s return statement)
- value: optional string (the value returned by the entry point function, if any; present only if the return statement is reachable the entry point function does not return void, and the -no-results option has not been used for that function)
exit_function (information about calls to the _exit function)
- type: string = informative (information that may be interesting to look at)
- reachable: boolean (reachability of the _exit function’s return statement)
- exit_return_value: optional string (possible values returned through the _exit function, only available when any call to _exit is reachable)
val_profile (indicates the value of the -val-profile option used for the Value Analysis (either interpreter or analyzer).)
value_results (indicates whether the Value Analysis results were available to compute all other information. true if the -no-results option was not given, false otherwise.)
memory_usage (the peak virtual memory usage of the analyzer)
- words: integer (size in words)
- bytes: integer (size in bytes)
- kbytes: integer (size in kilobytes)
- Mbytes: integer (size in megabytes)
- Gbytes: integer (size in gigabytes)

About the Dead code¶

The statement table already holds information about the dead blocks (see About Statements), but it is summarized in its own table together with mode information about unreachable functions:

When the -info-dead options is used, some information is printed for each dead block of the current project.

Only basic information about dead blocks and dead functions are given here. See -dead-xxx options to compute details. The following list explains which information can be found in each column:

File: file where the dead block or function is.

Function: name of the function.

Number: number of statements inside the dead block. The values are integers.

Description: description about the dead block or unreachable function. The possible values are:

Specification is used: for a function that is unreachable since its specification of is used.

Function that may be called: for a function that is not reachable but with a call path from a reachable function, and/or with its address taken so it might be indirectly called.

Block in reachable function: The dead block is in a reachable function.

Function called from never called function: for a function is only called from functions that never called.

Function that cannot be called at all: for a function that cannot be called at all since there is no syntactic call statement to it, and its address is not used.

Function only called by unreachable: for a function is only called in the cycle of functions that cannot be called.

CallNumber: gives the number of function calls in the dead block. The values are integers.

The -info-csv-dead filename option export the same information into the given filename.

Some additional information can be computed by setting some -dead-xxx options (see the DEAD CODE section in All Options). Any of these options trigger the compilation, and the generated and printed information depend on the combination of their values as explained below.

Computing dead code information¶

The main information computed about the dead code is to determine for each function whether:

it is reachable (and may have dead blocks),
or it is unreachable, and:
- it cannot be called at all because there is no syntactic calls to it, and its address is not taken,
- it may be called (and more details are given about how).

The default is to examine all function of the analyzed application (excluding the libc functions), but the -dead-functions option may be used to compute information for a function subset.

More details on the dead blocks of the reachable functions are given depending of the setting of the -dead-xxx options.

Note

What is called a dead block here is not necessarily C block. It is a set of contiguous statements that are not reachable by the Value Analysis. See the documentation of the Dead Id, Dead code entry and Dead code exit columns in About Statements.

Some of these options are presented below.

About the tests¶

Most of the time, the entry points of a dead block are tests that are always evaluated to the same value (either always true or always false). With the -dead-bk-with-tests option, the expression and evaluation of these tests are printed. Moreover, with the -dead-bk-with-subexp option, the possible values of each sub-expression are also printed, and if the -dead-bk-with-defs option is set, the origin of the definitions of the involved variables are also computed (this last option requires the -whole-program-graph option to be set). All these elements may help to understand why this dead block is unreachable.

About the `__tis_dead__` attribute¶

The __tis_dead__ block attribute may be used to mark some blocks. The -dead-bk-with-tis-dead and -dead-bk-skip-tis-dead may then be used to report about those blocks or to ignore them if the attribute is used to mark expected dead blocks.

For instance, in this example, the attribute may mean that we do not care if this block is dead, since it normally should be:

if (p == NULL) { __blockattribute__(__tis_dead__);
  abort();
  }

Printing dead code information¶

Default output¶

With the -dead-compute option, the results are printed to stdout.

Output to JSON¶

With the -dead-json option, the same results are exporter in JSON format to the specified file.

Summary of the dead blocks¶

With the -dead-bk-summary option, only the list of the dead blocks (in reachable functions) are printed, with some details about each of them.

Generate justification file¶

When some functions cannot be called at all, a justification file can be generated by setting the -dead-justification option. This file can then be provided to tis-aggregate to justify that those functions cannot be reached.

About the Decisions¶

The information about the decisions is related to the MC/DC computation. For more information, please refer to MC/DC (Modified Condition/Decision Coverage).

When the -info-decisions options is used, some information is printed for each decision of the current project.

A decision is a test in the code either used in if or loop statements. It is composed of boolean conditions with boolean operators to combine them. Information about decisions is useful to compute MC/DC (Modified condition/decision coverage). It is only available when the -mcdc option has been used, which also require to have Value analysis results computed with the -whole-program-graph option.

The following list explains which information can be found in each column:

File: file where the decision is.

Line: line of the file where the decision is. The values are integers.

Function: name of the enclosing function.

#conditions: number of conditions in the decision. The values are integers.

Conditions: list of the statement number if the conditions inside the function.

Mixed: tells whether the decision uses only one kind of boolean operator among && and || or not. The possible values are:

simple: for the decisions that use only one kind of boolean operator. In this case, MC/DC is equivalent to C/DC.

mixed: for the decisions that use both && and ||. In this case, MC/DC requires more computation than C/DC.

#ok(branches): when the -mcdc-compute option has been used, tells how many conditions of the decision reaches the branch coverage The values are integers, where -1 means not available.

#ok(mcdc): when the -mcdc-compute option has been used, tells how many conditions of the decision reaches the MC/DC criteria The values are integers, where -1 means not available.

Traces: for mixed decisions, lists of traces of the conditions evaluation. The value is NA otherwise.When there are some traces, the elements inside the trace are separated by “+”, the traces are separated by “ “, and there is a “/” between the THEN traces and the ELSE traces.

The -info-csv-decisions filename option export the same information into the given filename.

About the Show Queries¶

The tis-info-show-xxx options provide ways to make queries in order to print specified things The following list gives the provided options:

-info-show-val: takes a list of comma separated queries, and print the value computed for each of them. A query is composed of two parts separated by a white space:

the first one specifies the program point. There are three ways to specify it:

by its internal number sid,

or by f@n where f is a function name, and n the number of the statement inside it,

or by filename:line_number.

the second part specifies the term to evaluate. The term is specified using the ACSL syntax, but is usually just a variable name.

Example: -info-show-val "f@1 x","g@3 y" print the value of x before the first statement of f, and the value of y before the third statement of g.

Notice that values are available only if the value analysis computed them.

-info-show-state: 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: print the selected statement for the queries that involve program points.

-info-show-with-callstack: show the detailed values for each call stack.

All Options¶

This is the result of the -info-help option that gives the list of all the available options:

Plug-in name: info
Plug-in shortname: info
Description: extract many information from the current project.

Most options of the form '-info-option-name' and without any parameter
have an opposite with the name '-info-no-option-name'.

Most options of the form '-option-name' and without any parameter
have an opposite with the name '-no-option-name'.

Options taking a string as argument should preferably be written
-option-name="argument".

***** LIST OF AVAILABLE OPTIONS:

-info-dead          print information about dead blocks. (opposite option is
                    -info-no-dead)
-info-decisions     print information about decisions (opposite option is
                    -info-no-decisions)
-info-exit-status   print information about the application exit status, and
                    exit points. Needs value analysis results. (opposite
                    option is -info-no-exit-status)
-info-files         print information about files from the current project.
                    (opposite option is -info-no-files)
-info-functions     print information about functions from the current
                    project. (opposite option is -info-no-functions)
-info-precision <n>  give information about loss of precision: 0 for none, 1
                    or more for more (defaults to 0)
-info-properties    print information about properties from the current
                    project. (opposite option is -info-no-properties)
-info-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. (opposite option is -info-no-reachable)
-info-shared-variables  print information about the shared variables after a
                    Mthread analysis (opposite option is
                    -info-no-shared-variables)
-info-statements    print information about statements (opposite option is
                    -info-no-statements)
-info-types         print information about types (opposite option is
                    -info-no-types)
-info-variables     print information about global variables (opposite option
                    is -info-no-variables)

*** CSV GENERATION

-info-csv-all <basename>  export all the computed information in csv files
                    with filenames based on the specified basename
-info-csv-dead <filename>  export information about dead blocks in the
                    specified csv file.
-info-csv-decisions <filename>  export information about decisions in the
                    specified csv file
-info-csv-files <filename>  export information about files in the specified
                    csv file
-info-csv-functions <filename>  export information about functions in the
                    specified csv file
-info-csv-properties <filename>  export information about properties in the
                    specified csv file
-info-csv-shared-variables <filename>  export information about shared
                    variables in the specified csv file
-info-csv-statements <filename>  export information about statements in the
                    specified csv file
-info-csv-types <filename>  export information about types in the specified
                    csv file
-info-csv-variables <filename>  export information about global variables in
                    the specified csv file

*** DEAD CODE

-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. (opposite option
                    is -no-dead-bk-skip-tis-dead)
-dead-bk-summary    Print a summary about dead code blocks in reachable
                    functions in CSV format. (opposite option is
                    -no-dead-bk-summary)
-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). (opposite option is
                    -no-dead-bk-with-defs)
-dead-bk-with-subexp  Print the values of the sub-expressions of the tests
                    (only if -dead-bk-with-tests). (opposite option is
                    -no-dead-bk-with-subexp)
-dead-bk-with-tests  Print the test expressions of the dead blocks. (opposite
                    option is -no-dead-bk-with-tests)
-dead-bk-with-tis-dead  Print information about the blocks marked with
                    `__blockattribute__(__tis_dead__)`. (opposite option is
                    -no-dead-bk-with-tis-dead)
-dead-compute       Print information about dead code. See other '-dead-xxx'
                    options with -info-help. to tune the details of the
                    computation. (opposite option is -no-dead-compute)
-dead-functions <f1,...,fn>  Name of the functions to examine. Examine all of
                    them by default.
-dead-json <filename>  Compute the same results than the -dead-compute
                    option, and print them to the given file using the JSON
                    format.
-dead-justification <filename>  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.

*** GETTING INFORMATION

-info-help          help of plug-in info
-info-h             alias for option -info-help
-info-help-dead     print help about getting information about dead blocks.
                    (opposite option is -info-no-help-dead)
-info-help-decisions  print help about getting information about decisions.
                    (opposite option is -info-no-help-decisions)
-info-help-files    print help about files information. (opposite option is
                    -info-no-help-files)
-info-help-functions  print help about functions information. (opposite
                    option is -info-no-help-functions)
-info-help-json-results  print help about the JSON format used in the file
                    generated when using the '-info-json-results' option.
                    (opposite option is -info-no-help-json-results)
-info-help-properties  print help about properties information. (opposite
                    option is -info-no-help-properties)
-info-help-reachable  print help about getting information about reachable
                    statements. (opposite option is -info-no-help-reachable)
-info-help-shared-variables  print help about getting information about
                    shared variables. (opposite option is
                    -info-no-help-shared-variables)
-info-help-show     print more help about the 'show' queries. (opposite
                    option is -info-no-help-show)
-info-help-statements  print help about getting information about statements.
                    (opposite option is -info-no-help-statements)
-info-help-types    print help about getting information about types.
                    (opposite option is -info-no-help-types)
-info-help-variables  print help about getting information about global
                    variables. (opposite option is -info-no-help-variables)

*** OUTPUT MESSAGES

-info-debug <n>     level of debug for plug-in info (defaults to 0)
-info-msg-key <k1[,...,kn]>  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-verbose <n>   level of verbosity for plug-in info (defaults to 1)

*** RESULTS

-info-json-results <filename>  export the -info-results results to the given
                    file using the JSON format.
-info-results       print an overview of the most important results of an
                    analysis. (opposite option is -info-no-results)
-info-results-skip-abort <f1,..,fn>  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 <f1,..,fn>  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 <re_1,..,re_n>  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 <p1,..,pn>  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.
-tis-report         generate all files needed by tis-report in directory
                    _results. This may be changed with the option
                    -tis-report-directory (opposite option is -no-tis-report)
-tis-report-basename <basename>  generate tis-report files with names based
                    on 'basename'.
                    Beware: ensure to set this option before the -tis-report
                    option.
-tis-report-directory <basedir>  generate tis-report files to directory
                    basedir.
                    Beware: ensure to set this option before the -tis-report
                    option. (defaults to _results)

*** SHOW QUERIES

-info-show-state <program_point>  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  print the selected statement for the queries that
                    involve program points. (opposite option is
                    -info-no-show-statements)
-info-show-val <"program_point term">  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  show the detailed values for each call stack.
                    (opposite option is -info-no-show-with-callstack)

*** TUNING

-info-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. (opposite option is
                    -info-no-compute)
-info-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. (opposite option is
                    -info-no-stmt-no-reduction)
-info-with-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. (set by default,
                    opposite option is -info-without-stat)
-info-without-stat  opposite of option "-info-with-stat"

tis-info Manual¶

Introduction¶

About Functions¶

About Statements¶

About Files¶

About Types¶

About Variables¶

About Shared Variables¶

About Properties¶

Examples¶

About Value analysis results¶

Errors¶

Section results:undef¶

Section results:degeneration¶

Section results:non-terminating¶

Section results:messages¶

Section results:alarms¶

More things to examine¶

Section results:hypotheses¶

Section results:no-body-but-spec¶

Section results:body-but-use-spec¶

Section results:builtins¶

Section results:useless-files¶

Some more information¶

Section results:coverage¶

Section results:precision¶

Section results:exits¶

JSON format¶

About the Dead code¶

Computing dead code information¶

About the tests¶

About the __tis_dead__ attribute¶

Printing dead code information¶

Default output¶

Output to JSON¶

Summary of the dead blocks¶

Generate justification file¶

About the Decisions¶

About the Show Queries¶

All Options¶

`tis-info` Manual¶

Section `results:undef`¶

Section `results:degeneration`¶

Section `results:non-terminating`¶

Section `results:messages`¶

Section `results:alarms`¶

Section `results:hypotheses`¶

Section `results:no-body-but-spec`¶

Section `results:body-but-use-spec`¶

Section `results:builtins`¶

Section `results:useless-files`¶

Section `results:coverage`¶

Section `results:precision`¶

Section `results:exits`¶

About the `__tis_dead__` attribute¶