The coverage reported by TrustInSoft Analyzer, expressed as:
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.Property of a loop that is verified in two steps:
requires
.ensures
.\return
pseudo-variable holds the returned value.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.