NPATH is a metric introduced by Brian A. Nejmeh (Communications of the ACM, 31(2):188-200, 1988) that is aimed at overcoming some important limitations of McCabe’s cyclomatic complexity metric. Despite the fact that the declared NPATH objective is to count the number of acyclic execution paths through a function, the definition given for the C language in Nejmeh’s paper fails to do so even for very simple programs. We show that counting the number of acyclic paths in CFG is unfeasible in general. Then we define a new metric for C -like languages, called $A C P A T H$, that allows to quickly compute a very good estimation of the number of acyclic execution paths through the given function. We show that, if the function body does not contain backward gotos and does not contain jumps into a loop from outside the loop (which is the case for all MISRA-compliant programs), then such estimation is actually exact.

Verification of C/C++ programs has seen considerable progress in several areas, but not for programs that use these languages’ mathematical libraries. The reason is that all libraries in widespread use come with no guarantees about the computed results. This would seem to prevent any attempt at formal verification of programs that use them: without a specification for the functions, no conclusion can be drawn statically about the behavior of the program. We propose an alternative to surrender. We introduce a pragmatic approach that leverages the fact that most math.h/cmath functions are almost piecewise monotonic: as we discovered through exhaustive testing, they may have glitches , often of very small size and in small numbers. We develop interval refinement techniques for such functions based on a modified dichotomic search, which enable verification via symbolic execution based model checking, abstract interpretation, and test data generation. To the best of our knowledge, our refinement algorithms are the first in the literature to be able to handle non-correctly rounded function implementations, enabling verification in the presence of the most common implementations. We experimentally evaluate our approach on real-world code, showing its ability to detect or rule out anomalous behaviors.