This patch adds two more SymbolData subclasses: SymIntExpr and SymSymExpr, for
representing symbolic expressions like 'x'+3 and 'x'+'y'. The design is
subjected to change later when we fix the class hierarchy of symbolic
expressions.
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@67678 91177308-0d34-0410-b5e6-96231b3b80d8
diff --git a/lib/Analysis/SimpleConstraintManager.cpp b/lib/Analysis/SimpleConstraintManager.cpp
index e6f940e..50552c1 100644
--- a/lib/Analysis/SimpleConstraintManager.cpp
+++ b/lib/Analysis/SimpleConstraintManager.cpp
@@ -21,28 +21,11 @@
SimpleConstraintManager::~SimpleConstraintManager() {}
bool SimpleConstraintManager::canReasonAbout(SVal X) const {
- if (nonloc::SymIntConstraintVal *Y = dyn_cast<nonloc::SymIntConstraintVal>(&X)) {
- const SymIntConstraint& C = Y->getConstraint();
- switch (C.getOpcode()) {
- // We don't reason yet about bitwise-constraints on symbolic values.
- case BinaryOperator::And:
- case BinaryOperator::Or:
- case BinaryOperator::Xor:
- return false;
- // We don't reason yet about arithmetic constraints on symbolic values.
- case BinaryOperator::Mul:
- case BinaryOperator::Div:
- case BinaryOperator::Rem:
- case BinaryOperator::Add:
- case BinaryOperator::Sub:
- case BinaryOperator::Shl:
- case BinaryOperator::Shr:
- return false;
-
- // All other cases.
- default:
- return true;
- }
+ if (nonloc::SymbolVal* SymVal = dyn_cast<nonloc::SymbolVal>(&X)) {
+ const SymbolData& data
+ = getSymbolManager().getSymbolData(SymVal->getSymbol());
+ return !(data.getKind() == SymbolData::SymIntKind ||
+ data.getKind() == SymbolData::SymSymKind );
}
return true;
@@ -143,6 +126,12 @@
const GRState*
SimpleConstraintManager::AssumeAux(const GRState* St,NonLoc Cond,
bool Assumption, bool& isFeasible) {
+ // We cannot reason about SymIntExpr and SymSymExpr.
+ if (!canReasonAbout(Cond)) {
+ isFeasible = true;
+ return St;
+ }
+
BasicValueFactory& BasicVals = StateMgr.getBasicVals();
SymbolManager& SymMgr = StateMgr.getSymbolManager();