steakhal wrote: > What kind of effort is needed to make the z3 backend suitable to be supported?
I think, at minimum, we should be able to set Z3 as the default solver and run all the tests we have in `check-clang-analysis`. It will fail them of course because it doesn't meet the expectations but it must not crash. Once we have that, we can look at the open GH issues and check if any of those are still valid and fix them. After that, we should try to analyze clang itself, and if it still crashes, fix those too. After all this, I think we would have someone who built up enough experience in that part of the codebase to say that we have expertise. The last remaining component would be have someone around who is willing to invest into triaging and potentially fixing incoming issues wrt. the Z3 solver. As a bonus, one could look into performance anomalies that the Z3 solver is known for - but I'd say that fixing crashes is more important than slow analysis or hangs. https://github.com/llvm/llvm-project/pull/205370 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
