ddcc added a comment. > @ddcc To be completely honest, I see a few design issues with the current > implementation of Z3 backend, > the main one being that it checks satisfiability after every single exploded > node. > To the best of my knowledge, reasonable scalability would not be achieved > with such an approach, > and I'm not sure how feasible would it be to change it without rewriting > most of the checkers.
I agree, though a number of these are limitations in CSA, and not specifically the backend. > Thus we currently do not plan to set up a Z3 bot, but if you wish to maintain > we certainly can provide pointers on how this can be done. I don't plan to set one up either. Just compiling clang/llvm is already very resource intensive. > What do you think if we introduce `ninja check-clang-analyzer` to run the > analyzer tests, and `ninja check-clang-analyzer-z3` to run all the analyzer > tests with Z3? > [there might be another ninja target for running all analyzer tests, I just > don't remember which one. But at the end of the day there should be away to > run analyzer tests without Z3 even when Z3 is linked in] Sounds good. Repository: rC Clang https://reviews.llvm.org/D47726 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
