Improving the Accuracy of Library Function Modeling in the Static Analyzer
M. G. Biktimirov, Valery Nikolayevich Ignatyev, M. V. Belyaev · 2023
Program's source code usually contains many calls of library functions without available sources, therefore there is no way to analyze them like user code. To achieve accuracy required by industrial static analyzer, various library modeling methods are used. The paper presents one of the methods used by the SharpChecker static source code analyzer for modeling library functions using C# specifications in the symbolic execution engine. The approach allows to store and explore predicates of events, important side-effects and other information useful for error detectors with reasonable accuracy. It makes it possible to model side-effects of user-defined lambda-functions passed to external methods as parameters, which is especially important for frequently used C# LINQ methods. The effectiveness of these improvements was evaluated on the set of open source projects containing 6 million lines of code.