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; 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