NoQ added a comment. In D85528#2204664 <https://reviews.llvm.org/D85528#2204664>, @steakhal wrote:
> In D85528#2203325 <https://reviews.llvm.org/D85528#2203325>, @NoQ wrote: > >> Because this patch changes the behavior of regular analysis (without Z3), i >> expect tests to reflect that. > > What do you expect exactly? > > `REQUIRES: z3` is necessary for the refutation. > However, adding this requirement would not mean that this test will run if > you have Z3 installed though. > You should add the extra `llvm-lit` param to enable such tests. > I don't want to repeat myself too much but D83677 > <https://reviews.llvm.org/D83677> describes all the details of this test > infra fiasco. > I would appreciate some feedback there. I expect at least one LIT test //without// `-analyzer-config crosscheck-with-z3=true` (i.e., tests the default behavior, not the Z3 behavior) and works differently before and after the patch. Because you are introducing a change in the default behavior: an unknown value is now denoted by a different symbolic value. And the default behavior is much more important to cover with tests than the non-default behavior - simply because it's the default behavior, which means the vast majority of our users will notice the change. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D85528/new/ https://reviews.llvm.org/D85528 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
