};
class SymbolConjured : public SymbolData {
- Stmt* S;
+ const Stmt* S;
QualType T;
unsigned Count;
const void* SymbolTag;
public:
- SymbolConjured(SymbolRef Sym, Stmt* s, QualType t, unsigned count,
+ SymbolConjured(SymbolRef Sym, const Stmt* s, QualType t, unsigned count,
const void* symbolTag)
: SymbolData(ConjuredKind, Sym), S(s), T(t), Count(count),
SymbolTag(symbolTag) {}
- Stmt* getStmt() const { return S; }
+ const Stmt* getStmt() const { return S; }
unsigned getCount() const { return Count; }
const void* getTag() const { return SymbolTag; }
QualType getType(ASTContext&) const;
- static void Profile(llvm::FoldingSetNodeID& profile, Stmt* S, QualType T,
- unsigned Count, const void* SymbolTag) {
+ static void Profile(llvm::FoldingSetNodeID& profile, const Stmt* S,
+ QualType T, unsigned Count, const void* SymbolTag) {
profile.AddInteger((unsigned) ConjuredKind);
profile.AddPointer(S);
profile.Add(T);
/// Make a unique symbol for MemRegion R according to its kind.
SymbolRef getRegionRValueSymbol(const MemRegion* R);
- SymbolRef getConjuredSymbol(Stmt* E, QualType T, unsigned VisitCount,
+ SymbolRef getConjuredSymbol(const Stmt* E, QualType T, unsigned VisitCount,
const void* SymbolTag = 0);
- SymbolRef getConjuredSymbol(Expr* E, unsigned VisitCount,
+ SymbolRef getConjuredSymbol(const Expr* E, unsigned VisitCount,
const void* SymbolTag = 0) {
return getConjuredSymbol(E, E->getType(), VisitCount, SymbolTag);
}
BinaryOperator::Opcode Op = U->isIncrementOp() ? BinaryOperator::Add
: BinaryOperator::Sub;
- SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U));
+ SVal Result = EvalBinOp(Op, V2, MakeConstantVal(1U, U));
+
+ // Conjure a new symbol if necessary to recover precision.
+ if (Result.isUnknown() || !getConstraintManager().canReasonAbout(Result))
+ Result = SVal::GetConjuredSymbolVal(SymMgr, Ex,
+ Builder->getCurrentBlockCount());
+
state = BindExpr(state, U, U->isPostfix() ? V2 : Result);
// Perform the store.
return UnknownVal();
}
+SVal SVal::GetConjuredSymbolVal(SymbolManager &SymMgr, const Expr* E,
+ unsigned Count) {
+
+ QualType T = E->getType();
+
+ if (Loc::IsLocType(T)) {
+ SymbolRef Sym = SymMgr.getConjuredSymbol(E, Count);
+ return loc::SymbolVal(Sym);
+ }
+ else if (T->isIntegerType() && T->isScalarType()) {
+ SymbolRef Sym = SymMgr.getConjuredSymbol(E, Count);
+ return nonloc::SymbolVal(Sym);
+ }
+
+ return UnknownVal();
+}
+
nonloc::LocAsInteger nonloc::LocAsInteger::Make(BasicValueFactory& Vals, Loc V,
unsigned Bits) {
return LocAsInteger(Vals.getPersistentSValWithData(V, Bits));