xazax.hun added a comment. 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) #x00000010) (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. 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
