[analyzer] Fix assertion failure in SMT conversion for unary operator on floats
In the handling of the Symbols from the RangExpr, the code assumed that the operands of the unary operators need to have integral type. However, the CSA can create SymExpr with a floating point operand, when the integer value is cast into it, like `(float)h == (float)l` where both of `h` and `l` are integers. This patch handles such situations, by using `fromFloatUnOp()` instead of `fromUnOp()`, when the operand have a floating point type. I have investigated all other calls of `fromUnOp()`, and for one in: - `getZeroExpr()` is applied only on boolean types, so it correct - `fromBinOp()` is not invoked for floating points - `fromFloatUnOp()` I am uncertain about this case and I was not able to produce a test that would reach this point, as a negation of floating points numbers seem to produce `Unknown` symbols. This issue exists since the introduction of `UnarySymExpr` in D125318 and their handling for Z3 in D125547. Patch by Tomasz Kamiński. Reviewed By: mikhail.ramalho Differential Revision: https://reviews.llvm.org/D140891
Loading
Please sign in to comment