vsavchenko added a comment. 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? > > For example: > > (declare-const a ( _ BitVec 32 )) > (declare-const b ( _ BitVec 32 )) > > ; Assume 0 <= a, b, <= 5 > (assert (bvsge a #x00000000)) > (assert (bvsge b #x00000000)) > (assert (bvsle a #x00000005)) > (assert (bvsle b #x00000005)) > > ; Check if 0 <= a + b <= 10 > (assert (not (and (bvsle (bvadd a b) #x0000000A) (bvsge (bvadd a b) > #x00000000)))) > > (check-sat) > > Of course, the example above is obvious, but with overflows and other corner > cases it is great to have a tool doublecheck our assumptions, and share how > to reproduce the results. I usually add things like this not about the tests, but about the implementation. I think it provides a bit more generality. But usually I do it as a comment to the patchset, maybe it is also good to put it in the code as well. 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? 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
