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

This revision was landed with ongoing or failed builds. This revision was automatically updated to reflect the committed changes. Closed by commit rGcd5783d3e82b: [analyzer][solver] Handle UnarySymExpr in SMTConv (authored by martong). Repository: rG LLVM Github Monorepo CHANGES SINCE LAST

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

martong updated this revision to Diff 432019. martong marked an inline comment as done. martong added a comment. - Compare the size of the types instead of the type pointers Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D125547/new/

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

martong marked an inline comment as done. martong added inline comments. Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:463 + // has a different type than the unary itself. + if (OperandTy != Sym->getType()) { +if (hasComparison)

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

steakhal accepted this revision. steakhal added a comment. I think it looks greatt There are a couple questions you need to think about, but I don't insist about changing anything if the code works passed widescale testing. Comment at:

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

martong updated this revision to Diff 431970. martong added a comment. - Fix Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"' failed. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D125547/new/

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

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

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

martong added a comment. In D125547#3515259 , @steakhal wrote: > Something is messed up with the diff. You refer to `fromUnOp()` but it's not > defined anywhere. No. There is no mess up here, the diff is correct. `fromUnOp` had been implemented way

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

steakhal added a comment. Something is messed up with the diff. You refer to `fromUnOp()` but it's not defined anywhere. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D125547/new/ https://reviews.llvm.org/D125547

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

martong updated this revision to Diff 429633. martong marked 2 inline comments as done. martong added a comment. - Use existing fromUnOp - pass nullptr as FromTy Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D125547/new/

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

martong marked 2 inline comments as done. martong added inline comments. Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:258 + static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef , + ASTContext ,

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

steakhal accepted this revision. steakhal added a comment. This revision is now accepted and ready to land. minor nits; Thanks Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:258 + static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef , +

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

martong created this revision. martong added reviewers: steakhal, NoQ, mikhail.ramalho. Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy, Szelethus, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun. Herald added a reviewer: Szelethus. Herald added a project: