Static checker of semantic run-time errors

Static error analyzers are often considered an effective tool for improving the quality of programs together with well-known means of testing and debugging. However, the available run-time error analyzers cannot find the majority of real errors and are able to generate only long lists of warnings, which makes their application ineffective. In this paper, we determine the conditions under which a potential error found in the process of the program analysis is a definite error. It turns out that definite errors can be found only for definite variable definitions. Relaxation of the conditions of the error certainty determines a practically important class of so-called conditional errors, which prove to be definite errors in one case out of five on the average. An effective algorithm for powerful context-sensitive data flow analysis with the approximation of definite variable definitions is developed. A static analyzer based on the data flow analysis is developed for analyzing programs written in the mixture of the languages Oberon-2 and Medula-2 in the development environment XDS for OS/2, Windows 95/NT, and SunSparc. This analyzer is called OSA (Oberon-2/Modula-2 Static Analyzer); it is available at http://www.xds.ru/osa/. The analyzer has been successfully used to analyze real programs. In particular, it found 32 errors of various kinds in two programs of OBERON System 3 (about 26000 code lines in total) that has been in intensive use for three years.