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.
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.
Local property to check at a program point.
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 condition coverage.
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 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 (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.
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.
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 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.
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.
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 contract composed of preconditions, postconditions, and assigns properties expressed in ACSL.
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.
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.
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.
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.
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.
The same as syntactically 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)
}
}
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.
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.
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.
Refers to the memory state that holds the values of all the variables and allocated memory at that point in the program.
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.
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 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.
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
}
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.
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.
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.
The same as syntactically unreachable.
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:
semantically unreachable—uncallable given the current set of input vector,
syntactically unreachable—uncallable for any input vector, or
transitively syntactically unreachable—uncallable for any input vector, because all the function’s potential callsites fall inside other syntactically unreachable functions.
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)
}
}
Static analysis that computes an over-approximation of the states at each reachable program point using Abstract Interpretation theory.
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.
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.