manas added a comment. In D103440#2800710 <https://reviews.llvm.org/D103440#2800710>, @vsavchenko wrote:
> In D103440#2800122 <https://reviews.llvm.org/D103440#2800122>, @manas wrote: > >> In D103440#2799629 <https://reviews.llvm.org/D103440#2799629>, @xazax.hun >> wrote: >> >>> I was wondering, if we could try something new with the tests. To increase >>> our confidence that the expected behavior is correct, how about including a >>> Z3 proof with each of the test cases? >> >> We are looking forward to design a unit-test framework for the solver which >> can compact the test cases and make them much more manageable (unlike >> `constant-folding.c`). Perhaps, we can incorporate the Z3 proves in that >> framework, corresponding to test cases. > > Hmm, so you mean we can check if the analyzer was compiled with Z3 and if so, > verify the same things by it? Yeah in some sense. But I think that having proof for every test case may become redundant for certain cases. For e.g., consider two test cases for addition operator: 1. c == [0, 10] and d == [-10, 0] will result in (c + d) == [-10, 10] 2. c == d == [0, 10] will result in (c + d) == [0, 20] But the first test case can be modeled as `c - (- d)`or `c - D`, that is, - usage of subtraction binary operator : (c **-** D), and - symmetrical inversion of range around origin (**-** d) for symbol `d`. This will shift the range from `[-10, 0]` to `[0, 10]`. Considering having proof for every test case will make the proof for test-case 1 kind of redundant. So, I think we should go with @vsavchenko 's method of adding Z3 proof with the **implementation** (in code), instead of test cases themselves. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D103440/new/ https://reviews.llvm.org/D103440 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
