Vlad Tsyrklevich Twitter, GitHub, Keybase, e-mail
A second look at clang analyzer: Z3 constraint manager

It's been over year since my last post talking about my first experience with clang analyzer. In the last post I mentioned that Dominic Chen was introducing a Z3 constraint manager. It's been in clang for over a year now and I recently started trying to use it.

TODO: quick explanation of the constraint manager/path-sensitive analysis, simple can be like: int arr[5]; if (idx < 5) arr[idx] = 0;

TODO: Explain process of using them. Two crashes at first that are fixed on trunk (or 7.0 when it omes out)

TODO: Remind of the kernel checkers, not super succesful but easy things to use to test changes like this. Some quick benchmarks. Some Linux files veeeeery slow.

TODO: Link to dddc and Mikhail's pages to show their commits. Mention Mikhail's project (hopefully will cause more analyzer devs to use Z3 and help keep it working/tested)

Dominic Chen changes: https://reviews.llvm.org/differential/?authors=PHID-USER-ryohwzy7kxxwg5secws4#R Mikhail changes: https://reviews.llvm.org/differential/query/RDVbGdNVjNYm/#R Mikhail GSoC project: https://lists.llvm.org/pipermail/cfe-dev/2018-May/057831.html

Published on 27 Mar 2017