The ANSI/ISO C Specification Language, described in the ACSL Documentation.
Properties generated by TrustInSoft Analyzer and expressed in the ACSL logic language. For the program to be correct, the properties need to hold at a given point in the program. An alarm is a property that TrustInSoft Analyzer could not guarantee to be held.
Local property to check at a program point.
Assigns property
Property that specifies an over-approximation of the data that are modified by a function. The data that are not part of the assigns properties have the same value in the pre-state and post-state.
See Function specification.
Coverage analysis

The coverage reported by TrustInSoft Analyzer, expressed as:

  • Function coverage: percentage of the functions.
  • Statement coverage: percentage of the statements.
  • Semantic statement coverage: percentage of the statments in the reachable functions.
The Common Weakness Enumeration is a dictionary of common software weaknesses maintained by the MITRE Corporation.
The CWE subset covered by TrustInSoft Analyzer is described in the CWE Coverage document.
Can be specified in the right part of an assigns property, after the \from keyword. The property states that if the function is executed with two different pre-states, but where the dependencies have the same values, then the modified data has the same value in the two post-states.
Function specification
Function contract composed of preconditions, postconditions, and assigns properties expressed in ACSL.
Loop invariant

Property of a loop that is verified in two steps:

  • The establishment ensures that it is true before the loop.
  • The preservation ensures that if it is true at the beginning of any iteration, then it is also true at the beginning of the next one.
Property that must be satisfied in the pre-state. It is defined in the function specification with the keyword requires.
The state when entering a function. The formal parameters hold the input values, but the local variables are not defined yet.
Property that must be satisfied in the post-state. It is defined in the function specification with the keyword ensures.
The state at the end of a function. The local variables don’t exist anymore, the formal parameters have the same value than in the pre-state (because the arguments are passed by value in C), the \return pseudo-variable holds the returned value.
Computation of the set of program statements, the program slice, that may affect the values at some point of interest, referred to as a slicing criterion. The result is another program that is guaranteed to compile.
Refers to the memory state that holds the values of all the variables and allocated memory at that point in the program.
The Time Of Check to Time Of Use is a class of issues caused by a race condition between the check of a condition and the use of the results of that check.
Undefined Behavior

According to the ISO C11 standard, an undefined behavior is:

A behavior, upon use of a non-portable or erroneous program construct or of erroneous data, for which this International Standard imposes no requirements.

The C FAQ defines an undefined behavior as:

Anything at all can happen; the Standard imposes no requirements. The program may fail to compile, or it may execute incorrectly (either crashing or silently generating incorrect results), or it may fortuitously perform exactly what the programmer intended.

In C and C++, undefined behaviors are mainly associated to illegal operations leading to crashes such as accessing a null pointer or dividing by zero. However, they also include the interactions with compilers and their aggressive optimizations assuming that the program is not in an illegal state leading to security vulnerabilities.

Value analysis
Static analysis that computes an over-approximation of the states at each reachable program point using Abstract Interpretation theory.
The Weakest Precondition calculus is a method to verify a program property. It provides a mathematical formula that ensures that the property is true on the program as long as the formula is satisfied.