UNO: Static Source Code Checking for User-Defined Properties 1
Gerard J. Holzmann, Murray Gardner Hill · 2002
Only a small fraction of the output generated by typical static analysis tools tends to reveal serious software defects. Finding the important defects in a long list of warnings can be a frustrating experience. The output often reveals more about the limitations of the analyzer than about the code being analyzed. There are two main causes for this phenomenon. The first is that the typical static analyzer casts its nets too broadly, reporting everything reportable, rather than what is likely to be a true bug. The second cause is that most static analyzers can check the code for only a predetermined, fixed, set of bugs: the user cannot make the analyzer more precise by defining and experimenting with a broader range of application-dependent properties. We describe a source code analyzer called UNO that tries to remedy these problems. The default properties searched for by UNO are restricted to the three most common causes of serious error in C programs: use of uninitialized variables, nil-pointer dereferencing, and out-of-bound array indexing. The checking capabilities of UNO can be extended by the user with the definition of application-dependent properties, which can be written as simple ANSI-C functions.