Every program analysis technique has to finely balance the issues of scalability and precision. These issues are at odds with each other, and it is often difficult to find a suitable balance. This task can be simplified in some situations if we allow for occasional unsoundness of the analysis: that is, false positives. Such analysis can be quite precise and scale to multimillion-line programs, but typically cannot provide guarantees of soundness. The impact of these analyses is in the fact that they are able to detect bugs in real-world applications, while keeping the noise of false-positive results to manageable levels.

Saber, described in this paper, is the next step in the gradual evolution of bug-finding applications that analyze source-to-sink flows in programs and detect violations of particular policies governing such flows. In particular, Saber focuses on discovering memory leaks in programs. Saber has a lot of similarities with Fastcheck, from which it borrows a number of ideas. Similar to Fastcheck, it builds a value-flow graph and uses graph reachability to check for memory leaks; it analyzes each allocation site separately, allowing it to be applicable in an interactive setting; and it uses similar data structures and the overall flow of the analysis is similar.

Saber differs from its predecessors in the particular choices it makes for representing memory regions, the finer distinctions it makes for treating pointer expressions, and its use of different techniques for solving conditions annotating edges. These differences result in a system that seems to provide a better balance between scalability, precision, and false positives.