george.karpenkov added a subscriber: mikhail.ramalho.
george.karpenkov 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.

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.

> The test approach is what @dcoughlin suggested in 
> https://reviews.llvm.org/D28952, where the tests are run using each 
> constraint manager that is available

Apologies for conflicting instruction. Now that @mikhail.ramalho is working on 
refutation with Z3 it might not make sense to force the user to run all tests 
with Z3 at all times.
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]


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

Reply via email to