if (const auto *SSE = dyn_cast<SymSymExpr>(Sym)) {
BinaryOperator::Opcode Op = SSE->getOpcode();
- assert(BinaryOperator::isComparisonOp(Op));
-
- // We convert equality operations for pointers only.
- if (Loc::isLocType(SSE->getLHS()->getType()) &&
- Loc::isLocType(SSE->getRHS()->getType())) {
- // Translate "a != b" to "(b - a) != 0".
- // We invert the order of the operands as a heuristic for how loop
- // conditions are usually written ("begin != end") as compared to length
- // calculations ("end - begin"). The more correct thing to do would be to
- // canonicalize "a - b" and "b - a", which would allow us to treat
- // "a != b" and "b != a" the same.
-
- SymbolManager &SymMgr = getSymbolManager();
- QualType DiffTy = SymMgr.getContext().getPointerDiffType();
- SymbolRef Subtraction =
- SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
-
- const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
- Op = BinaryOperator::reverseComparisonOp(Op);
- if (!Assumption)
- Op = BinaryOperator::negateComparisonOp(Op);
- return assumeSymRel(State, Subtraction, Op, Zero);
- }
+ if (BinaryOperator::isComparisonOp(Op)) {
+
+ // We convert equality operations for pointers only.
+ if (Loc::isLocType(SSE->getLHS()->getType()) &&
+ Loc::isLocType(SSE->getRHS()->getType())) {
+ // Translate "a != b" to "(b - a) != 0".
+ // We invert the order of the operands as a heuristic for how loop
+ // conditions are usually written ("begin != end") as compared to length
+ // calculations ("end - begin"). The more correct thing to do would be
+ // to canonicalize "a - b" and "b - a", which would allow us to treat
+ // "a != b" and "b != a" the same.
+
+ SymbolManager &SymMgr = getSymbolManager();
+ QualType DiffTy = SymMgr.getContext().getPointerDiffType();
+ SymbolRef Subtraction =
+ SymMgr.getSymSymExpr(SSE->getRHS(), BO_Sub, SSE->getLHS(), DiffTy);
+
+ const llvm::APSInt &Zero = getBasicVals().getValue(0, DiffTy);
+ Op = BinaryOperator::reverseComparisonOp(Op);
+ if (!Assumption)
+ Op = BinaryOperator::negateComparisonOp(Op);
+ return assumeSymRel(State, Subtraction, Op, Zero);
+ }
- if (BinaryOperator::isEqualityOp(Op)) {
- SymbolManager &SymMgr = getSymbolManager();
+ if (BinaryOperator::isEqualityOp(Op)) {
+ SymbolManager &SymMgr = getSymbolManager();
- QualType ExprType = SSE->getType();
- SymbolRef CanonicalEquality =
- SymMgr.getSymSymExpr(SSE->getLHS(), BO_EQ, SSE->getRHS(), ExprType);
+ QualType ExprType = SSE->getType();
+ SymbolRef CanonicalEquality =
+ SymMgr.getSymSymExpr(SSE->getLHS(), BO_EQ, SSE->getRHS(), ExprType);
- bool WasEqual = SSE->getOpcode() == BO_EQ;
- bool IsExpectedEqual = WasEqual == Assumption;
+ bool WasEqual = SSE->getOpcode() == BO_EQ;
+ bool IsExpectedEqual = WasEqual == Assumption;
- const llvm::APSInt &Zero = getBasicVals().getValue(0, ExprType);
+ const llvm::APSInt &Zero = getBasicVals().getValue(0, ExprType);
- if (IsExpectedEqual) {
- return assumeSymNE(State, CanonicalEquality, Zero, Zero);
- }
+ if (IsExpectedEqual) {
+ return assumeSymNE(State, CanonicalEquality, Zero, Zero);
+ }
- return assumeSymEQ(State, CanonicalEquality, Zero, Zero);
+ return assumeSymEQ(State, CanonicalEquality, Zero, Zero);
+ }
}
}