Tutorials

This section provides step-by-step tutorials to help you get started with TrustInSoft Analyzer.

The goal of TrustInSoft Analyzer is to prevent runtime errors by analyzing all of the possible values that the variables can take at any given point in the program, in order to prove that none of the execution paths leads to a problem (such as an undefined behavior or a forbidden operation).

This verification is called the value analysis.

Note

Unlike testing or binary analysis, the value analysis provided by TrustInSoft Analyzer is exhaustive: the guarantees provided apply to all the concrete executions of the program. Even the tests with the best coverage will only test a few execution paths in a program, whereas binary analysis is strongly dependent on the compilation and execution environments. This is why static value analysis gives stronger guarantees than both testing and binary analysis.

The value analysis will try to prove all the properties needed for the code to be correct. If a property can not be automatically proved, the analyzer will emit an alarm, such as:

/*@ assert Value: division_by_zero: b ≢ 0; */

It means that, in order for the program to be correct, the value of b needs to be non-zero at the point in the execution pointed by the analyzer.

At this point there are two possibilities:

  1. There is an execution path for which b = 0 that will lead to an error or an undefined behavior.

    This means there is a bug in the program that needs to be corrected in order to ensure that the property will hold.

  2. There is no execution path for which b = 0, but the analyzer was not able to prove the validity of the property.

    This means that the analyzer over-approximates the possible values of b, and in order to make the alarm disappear, it will be necessary to guide the analyzer to be more precise on the possible values of b, and then run the analysis again.

Tip

An alarm is a property, expressed in a logic language, that needs to hold at a given point in the program in order for the program to be correct.