Detecting memory and resource leaks in the Svace static analyzer

N. E. Malyshev^ab, A. E. Borodin^b, A. A. Belevancev^ab, V. A. Semenov<sup>cb

a</sup> Lomonosov Moscow State University
^b Ivannikov Institute for System Programming of the RAS
^c Moscow Institute of Physics and Technology

Abstract: The paper presents an approach to detecting memory and other resource leaks in the Svace static analyzer. We lay down a set of static analysis requirements that show the philosophy behind Svace, briefly describe the main analysis infrastructure based on an interprocedural symbolic execution with state merging, and show how this infrastructure can be applied to leak detection. We list attributes that are computed during analysis and present how this computation is performed, how allocation and release functions are modeled via specifications, how escaped memory is accounted for. We propose a way to provide external information not present in the source code to the analyzer via creating artificial functions. Experimental results on the Juliet test suite and the Binutils package show the viability of our ideas.

Keywords: static analysis, symbolic execution, memory leak, path sensitivity, dataflow analysis, points-to analysis.

DOI: 10.15514/ISPRAS-2025-37(3)-20