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.

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.