Detection of incorrect pointer dereferences for C/C++ programs using static code analysis and logical inference

This article considers a method for an increase of static code analysis precision. The method extends classic code analysis algorithm with dependency analysis. For this purpose, during abstract interpretation information about statically known values should be extracted as well as dependencies between unknown values. Dependencies can be represented with first-order logic predicates. Such a method allows using of external logical inference tools to prove truth or falsehood of branch conditions and of error occurrence conditions. The main focus is oriented to pointer analysis logic and incorrect dereference detection rules. A prototype is implemented and results of efficiency evaluation are provided. The prototype uses Microsoft Z3 Solver as a logical inference tool. A significant precision increase is shown, ways for performance boosting are suggested.