ddcc added a comment. I added support for a callback field in lit's configuration (see https://reviews.llvm.org/D29684), which is used to execute each testcase for each supported constraint solver backends at runtime. I believe this resolves all remaining issues, except for the remaining two testcase failures:
1. The testcase Analysis/reference.cpp currently fails, because the RangeConstraintManager has an internal optimization that assumes references are known to be non-zero (see RangeConstraintManager.cpp:422). This optimization is probably in the wrong place, and should be moved into the analyzer and out of the constraint solver. Unless anyone objects, I plan to modify this testcase so that this result is fine for the z3 solver backend. 2. The testcase Analysis/ptr-arith.c currently fails, because handling of ptrdiff_t is somewhat tricky. This constraint manager interface maps ptrdiff_t to a signed bitvector in Z3, and pointers to unsigned bitvectors in Z3. However, since this testcase compares the pointer values both directly and indirectly via ptrdiff_t, if a < b is true using a signed comparison, the same is not necessarily true using an unsigned comparison. Likewise, unless anyone objects, I plan to whitelist this result for the z3 solver backend. https://reviews.llvm.org/D28952 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
