Glossary

ACSL

The ANSI/ISO C Specification Language, described in the ACSL Documentation.

Alarms

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.

Analysis coverage

Analysis coverage is a measure of the proportion of statements or functions visited by the analyzer while performing a suite of analyses on some program with a specific set of vectors of inputs.

The coverage reported by TrustInSoft Analyzer is expressed as four modules:

TrustInSoft Analyzer can also optionally compute branch coverage and modified condition/decision coverage for individual decisions in the code base.

Assertion

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.

Branch coverage

See condition coverage.

CIL

See C Intermediate Language.

C Intermediate Language

The C Intermediate Language is a subset of C that constitutes the intermediate representation on which TrustInSoft Analyzer performs analyses. A CIL representation of a code base is constructed to remove ambiguity and implicitness from the code to which facilitates both the analysis itself and the interpretation of the results. The Analyzer translates C, C++, as well as Java into CIL. You encounter CIL when analyzing a code base through the GUI or when observing alerts.

Code coverage

Code coverage is a measure of the proportion of the code of a program that is executed during a given test suite with a specific set of vectors of inputs.

In the context of static analysis, code is not executed, but it is visited by the analyzer, so the appropriate term is analysis coverage. Nevertheless, we use both terms interchangeably when there is no risk of confusion.

Condition coverage

Condition coverage (aka branch coverage) is a code coverage criterion. It is applied to each decision in the code base separately and is satisfied if every leaf condition in that decision has taken on each possible outcome at least once. Condition coverage is a component of MC/DC coverage.

In the context of the analyzer condition coverage is satisfied for a given decision if each elementary leaf condition resulted in all possible outcomes at least once in the performed suite of analyses, evaluating once each to TRUE and FALSE or at least once to {TRUE, FALSE}.

Condition coverage can be reported per decision or in aggregate for the entire analyzed code base. For each decision, condition coverage can be expressed as the degree to which the decision satisfies the criterion as a percentage of how many leaf conditions were completely exercised. In aggregate, condition coverage expresses the ratio of decisions that satisfy the criterion vs. all decisions in the code base.

Condition coverage is referenced by ISO 26262, EN 50128, IEC 61508. This coverage criterion is further expanded by condition coverage and modified condition/decision coverage.

Contract

See function specification.

CWE

The Common Weakness Enumeration is a dictionary of common software weaknesses maintained by the MITRE Corporation.

CWE-subset

The CWE subset covered by TrustInSoft Analyzer is described in the CWE Coverage document.

Decision

A decision is an expression the evaluates to a Boolean value, which impacts the control flow of a program. A decision consists of one or more sub-expressions called leaf conditions.

Decision coverage

Decision coverage is a code coverage criterion. It is applied to each decision in the code base separately and is satisfied if the decision has taken on each possible outcome at least once. Decision coverage is a component of MC/DC coverage.

In the context of the analyzer condition coverage is satisfied for a given decision if it resulted in all possible outcomes at least once in the performed suite of analyses, evaluating once each to TRUE and FALSE or at least once to {TRUE, FALSE}.

TrustInSoft Analyzer does not calculate decision coverage, except as part of MC/DC. See MC/DC coverage for details.

Decision coverage is referenced by DO-178B and DO-178C. This coverage criterion is further refined by modified condition/decision coverage.

Dependencies

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 coverage

The ratio of functions visited by an analysis or a group of analyses vs. all functions defined in the analyzed code, expressed as a percentage. A component of analysis coverage.

Function specification

Function contract composed of preconditions, postconditions, and assigns properties expressed in ACSL.

Leaf condition

A leaf condition is an expression that evaluates to a Boolean value and cannot be broken down into simpler Boolean expressions. Leaf conditions are components of decisions.

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.

MC/DC

See modified condition/decision coverage.

Modified condition/decision coverage

Modified condition/decision coverage (MC/DC) is a code coverage criterion. It is applied to each decision in the code base separately and is satisfied if both condition coverage and decision coverage are satisfied, and if each leaf condition is shown to independently affect the outcome of its containing decision.

In the context of the analyzer MC/DC is satisfied for a given decision if:

  • the decision resulted in all possible outcomes at least once in the performed suite of analyses, evaluating once each to TRUE and FALSE or at least once to {TRUE, FALSE}—this means decision coverage is satisfied,

  • each elementary leaf condition resulted in all possible outcomes at least once in the performed suite of analyses—this means code coverage is satisfied,

  • each independent leaf conditions results in all possible outcomes, which affects the outcome of the decision while all other leaf conditions remain unchanged.

MC/DC can be reported per decision or in aggregate for the entire analyzed code base. For each decision, MC/DC can be expressed as the degree to which the decision satisfies the criterion as a percentage of how many leaf conditions were completely exercised and shown to independently affect the outcome of the decision . In aggregate, MC/DC expresses the ratio of decisions that satisfy the criterion vs. all decisions in the code base.

We provide more information about how TrustInSoft Analyzer calculates MC/DC in MC/DC coverage.

MC/DC coverage is a component (obligatory or optional) of multiple standards and guideline documents such as DO-178B/C, ISO 26262, and NPR 7150.2D.

Postcondition

Property that must be satisfied in the post-state. It is defined in the function specification with the keyword ensures.

Post-state

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.

Precondition

Property that must be satisfied in the pre-state. It is defined in the function specification with the keyword requires.

Pre-state

The state when entering a function. The formal parameters hold the input values, but the local variables are not defined yet.

Reachable

The same as syntactically reachable.

Semantically reachable

Semantic reachability describes whether or not a given function or statement could potentially be evaluated in some execution of the program starting from a specific entry point function and given a specific input vector. Semantic reachability is determined through value analysis, by evaluating expressions along the path from the entry point to the examined statement to narrow down whether execution could really proceed to a given statement or function.

The opposite of semantically unreachable.

If a statement or function is semantically reachable, it will be visited during the analysis.

If a statement or function is determined to be semantically reachable, it does not mean that it will be executed with the given vector of inputs, nor even that it is possible for it to be executed, but merely that value analysis could not exclude the possibility. However, if a statement or function are semantically unreachable, that guarantees that they cannot be executed given the specified input vector.

All semantically reachable statements and functions are syntactically reachable, but not vice versa.

An entry point function is always semantically reachable.

Example:

#include <stdio.h>

void f() {                            // Semantically reachable function    (if argc == 1)
  print("f");                         // Semantically reachable statement   (if argc == 1)
}

void g() {                            // Semantically unreachable function  (if argc == 1)
  print("g");                         // Semantically unreachable statement (if argc == 1)
}

int main (int argc, char argv[]) {    // Semantically reachable function    (entry point, argc == 1)
  if (argc) {                         // Semantically reachable statement
    f();                              // Semantically reachable statement   (if argc == 1)
  } else {
    g();                              // Semantically unreachable statement (if argc == 1)
  }
}
Semantically unreachable

The opposite of semantically reachable.

If a statement or function is semantically unreachable given some vector of inputs, it will be unvisited during an analysis with that vector of inputs.

If a statement or function are semantically unreachable, it is impossible for it to be evaluated during an execution of the program with the specified input vector.

Semantically unreachable statements and functions are never visited by value analysis.

Slicing

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.

Source line coverage

The ratio of lines of source code that contain a visited statement vs. all lines of code in the analyzed code base, expressed as a percentage. This is analogous to statement coverage, but calculated on lines of the original source code rather than CIL statements. A component of analysis coverage.

State

Refers to the memory state that holds the values of all the variables and allocated memory at that point in the program.

Statement coverage

The ratio of statements visited by an analysis or a group of analyses vs. all statements in the analyzed code, expressed as a percentage. A component of analysis coverage.

Statement coverage in reachable functions

The ratio of statements visited by an analysis or a group of analyses vs. all statements in all visited functions, expressed as a percentage. A component of analysis coverage.

Static analysis

Static analysis is an umbrella term for automated techniques that examine program code without executing the program. Static analysis techniques used by TrustInSoft Analyzer include value analysis and weakest precondition analysis.

Syntactically reachable

Syntactic reachability describes whether a given function or statement could potentially be evaluated in some execution of the program starting from a specific entry point function. In contrast to semantic reachability, syntactic reachability is determined irrespective of program inputs and without evaluating expressions along the path from the entry point to the examined statement or function call (with the exception of trivial expressions that would also be precomputed by the compiler, e.g. if (1) { … }).

While it is impossible for a syntactically unreachable statement or function to be evaluated during any execution of the program, a syntactically reachable function or statement does not imply the converse: it might be either possible or impossible to evaluate syntactically reachable code, but the possibility could not be precluded syntactically (e.g. without value analysis).

If a statement or function is syntactically reachable, it may or may not be visited during the analysis, depending on the input vector.

An entry point function is always syntactically reachable.

Example:

#include <stdio.h>

int f() {                             // Syntactically reachable function
  return 1;                           // Syntactically reachable statement
}

int g() {                             // Syntactically unreachable function
  return 0;                           // Syntactically unreachable statement
}

int main (int argc, char argv[]) {    // Syntactically reachable function (entry point)
  if (1) {                            // Syntactically reachable statement
    printf("a");                      // Syntactically reachable statement
  } else {
    printf("b");                      // Syntactically unreachable statement
  }
  if (argc) {                         // Syntactically reachable statement
    printf("c");                      // Syntactically reachable statement
  } else {
    printf("d");                      // Syntactically reachable statement
  }
  int v = f();                        // Syntactically reachable statement
  while (v) {                         // Syntactically reachable statement
    printf("e");                      // Syntactically reachable statement
  }
  printf("f");                        // Syntactically reachable statement
}
Syntactically unreachable

The opposite of syntactically reachable.

If a statement or function is not syntactically reachable, there is no possible execution of the program that would cause that statement or function to be evaluated, regardless of inputs.

If a statement or function is syntactically unreachable, it will not be visited during the analysis.

TOCTOU

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.

Unreachable

The same as syntactically unreachable.

Unvisited

In the context of a single value analysis with a specific vector of inputs, we say a statement or a function is unvisited, if it is not reached during the analysis.

In the context of multiple analyses being performed on the same code base, a statement or a function are unvisited, if they are not reached during any of the performed analyses.

The opposite of visited.

If a statement or function is unvisited by some analysis with some vector of inputs, it is semantically unreachable. Value analysis will not visit any semantically unreachable statements and functions.

An unvisited statement or a function will not be evaluated during any execution whose input vector is described by the input vectors of any of the performed analyses.

An unvisited function may be:

Example:

void f1() {       }                   // Visited function
void f2() { f3(); }                   // Unvisited function (semantically unreachable)
void f3() {       }                   // Unvisited function (semantically unreachable)
void f4() { f5(); }                   // Unvisited function (syntactically unreachable)
void f5() {       }                   // Unvisited function (second-hand syntactically unreachable)

int main (int argc, char argv[]) {    // Visited function   (entry point, argc == 1)
    if (argc) {                       // Visited statement
        f1();                         // Visited statement  (if argc == 1)
    } else {
        f2();                         // Unvisited statement  (if argc == 1)
    }
}
Value analysis

Static analysis that computes an over-approximation of the states at each reachable program point using Abstract Interpretation theory.

Visited

In the context of a single value analysis with a specific vector of inputs, we say a statement or a function is visited if it is reached (evaluated) during the analysis.

In the context of multiple analyses being performed on the same code base, we say a statement or a function is visited if it is reached by at least one of the performed analyses.

The opposite of unvisited.

If a statement or function is visited by some analysis with some vector of inputs, it is semantically reachable. Value analysis will visit all semantically reachable statements and functions.

A statement or a function being visited does not imply that it may actually be evaluated during some execution of the program. For example, a statement that cannot be executed in practice may be visited by the analyzer due to loss of precision during analysis.

Weakest Precondition

The Weakest Precondition calculus (WP) 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.