martong added a comment.
There are Z3 refutation related assertions on open-source projects once the
patch stack is applied. Interestingly it happens in `fromBinOp`.
clang-14:
../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:96:
static const llvm::SMTExpr*
clang::ento::SMTConv::fromBinOp(llvm::SMTSolverRef&, const llvm::SMTExpr*
const&, clang::BinaryOperator::Opcode, const llvm::SMTExpr* const&, bool):
Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have
the same sort!"' failed.
This is the minimal reproducer:
int b;
long c();
void d(int e, long *f) { *f = e; }
void k() {
long a = c();
int g = a, h = g - 2, i = -h;
_Bool j;
d(i, &b);
j &= b == 0;
}
I'd like to delay the commit of the patch stack until we can fix that, since Z3
refutation is essential for most of our (internal) users.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D125547/new/
https://reviews.llvm.org/D125547
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
