[PATCH] D28952: [analyzer] Add new Z3 constraint manager backend

Dominic Chen via Phabricator via cfe-commits cfe-commits at lists.llvm.org
Wed May 17 14:12:39 PDT 2017


ddcc added a comment.

In https://reviews.llvm.org/D28952#757375, @iris wrote:

> Thank you for helping me build clang with z3.I have already applied the above updating.But now I have another question, when running clang with '-Xanalyzer -analyzer-constraints=z3' there is always be a fatal error and I don't know whether it is right to use a command like 'clang -Xanalyzer -analyzer-constraints=z3 -analyzer-checker=debug.DumpExplodedGraph test.cpp-' to get the ExplodedGraph which is analyzed by z3constraint?Sorry to bother.


You probably want something along the lines of `clang --analyze -Xanalyzer -analyzer-constraints=z3 -Xanalyzer -analyzer-checker=debug.ViewExplodedGraph test.c`. In particular, there is a difference between using clang as a compiler driver or frontend (see FAQ entry on cc1 at https://clang.llvm.org/docs/FAQ.html). This is also mentioned in the checker development manual: https://clang-analyzer.llvm.org/checker_dev_manual.html .


Repository:
  rL LLVM

https://reviews.llvm.org/D28952





More information about the cfe-commits mailing list