[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

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