Modeling of library functions in an industrial static code analyzer

SharpChecker — это статический анализатор промышленного уровня, предназначенный для обнаружения различных ошибок в исходном коде C#. Поскольку инструмент активно разрабатывается, ему требуется все более точная информация о программной среде, особенно о результатах и побочных эффектах функций библиотеки. Статья посвящена эволюции моделей для стандартной библиотеки, исторически используемой SharpChecker, ее преимуществам и недостаткам. Мы начали с базы данных SQLite с наиболее важными свойствами функций, затем добавили написанные вручную реализации модели C# часто используемых методов для поддержки состояний контейнера данных, а недавно разработали модель, построенную на основе предварительного анализа исходного кода библиотеки, которая позволяет собрать все существенные побочные эффекты с условиями для почти всей библиотеки C#.