Abstract

This report describes the result of a case study using Monoidics’ tool Infer. The purpose of this case study is to gain experience with the Infer static analyzer produced by Infer.
For this case study, the SQLite open-source SQL database is analyzed and verified with the Infer static analyzer. Analysis of Infer’s reports resulted in bugs being submitted to the SQLite community and study provided the powerful tool of custom asserts to manipulate the verification process when necessary.
Chapter 2, the first Chapter of this report provides some background infor- mation about the SQLite project. It also includes a short description of the Infer static analyzer and the principles that make Infer work.
The process of the analysis of SQLite is described in Chapter 3 and Chapter 4 discusses the results and bugs obtained during this analysis.
Chapter 4.2.3 describes the experience with the SQLite community gained from submitting the bug reports.
Then Chapter 5 gives an overview of difficult programming patterns that were used by SQLite and a way to handle these patterns such that Infer will be able to properly deal with them.
Finally Chapter 6 describes the conclusions.