Interprocedural Pointer Analysis in Goanna

Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches, Goanna uses the off-the-shelf model checker NuSMV as its core analysis engine on a syntactic flow-sensitive program abstraction. The CTL-based model checking approach enables a high degree of flexibility in writing checks and scales to large code bases. In this paper, a new approach to pointer analysis for C is described. It is detailed how this technique is integrated into the model checking approach in order to perform interprocedural analysis. The performance and precision of this approach are demonstrated using a case study.