[analyzer] Eliminate analyzer limitations on symbolic constraint generation

[ddcc]

Summary

With the Z3 constraint manager, symbolic constraints can be fully reasoned about.

[ddcc]

Fix rebase

[ddcc]

Rebase

[ddcc]

Rebase

[xazax.hun]

Do you have a benchmark how this affects the performance and memory usage when the old constraint manager is used? I wonder if most of people are using the old one, it might make no sense to generate symbolic expressions that can not be solved anyway.
Maybe the analyzer could only generate these symbolic expressions when Z3 is used?

[ddcc]

It's been a while since I looked at the code, but I don't believe that all of the new constraints are necessarily unsupported by the current range constraint manager. Rather, they were just not being generated by the SimpleSValBuilder. The changes pass the testsuite for both the Range and Z3 constraint managers, without any special testcase handling that is Z3 specific.

Here are some runtime performance numbers on the testsuite:

Pre-Commit
RangeConstraintManager: 8.24s
Z3ConstraintManager: 247.29s

Post-Commit
RangeConstraintManager: 10.23s
Z3ConstraintManager: 250.35s

And for memory usage (max RSS):

Pre-Commit
edges-new.mm (RangeConstraintManager): 42688k
edges-new.mm (Z3ConstraintManager): 52916k
malloc-plist.c (RangeConstraintManager): 39812k
malloc-plist.c (Z3ConstraintManager): 50544k

Post-Commit
edges-new.mm (RangeConstraintManager): 43032k
edges-new.mm (Z3ConstraintManager): 52956k
malloc-plist.c (RangeConstraintManager): 40204k
malloc-plist.c (Z3ConstraintManager): 50364k

Edit: The Z3ConstraintManager runtime numbers are inflated, because I forgot that llvm-lit now runs both constraint managers with the new test setup. So the actual time for Z3 needs to have the RangeConstraintManager time subtracted out.

[ddcc]

Rebase

[ddcc]

Address SVal simplification from D31886

[ddcc]

I've updated this revision to account for the recent SVal simplification commit by @NoQ, but now there is an exponential blowup problem that prevents testcase PR24184.cpp from terminating, due to an interaction between Simplifier::VisitNonLocSymbolVal() and SValBuilder::makeSymExprValNN() when expanding the loop in case 3. I'm not quite sure what the best way to resolve this is; from some blind testing, I ended up needing to set MaxComp to 10 to force termination in a reasonable amount of time, but this restricts its usefulness for generating other symbolic constraints.

[ddcc]

Fix typo in SymbolCast simplification

[zaks.anna]

lib/StaticAnalyzer/Core/SValBuilder.cpp

357

I am concerned that removing the guard will regress performance in the vanilla case. (Note that Z3 support as well as taint are not on by default.)

I am curious how much of the regression you've measured could be gained back if we make this conditional.

364

Reducing the MaxComp is going to regress taint analysis..

I've updated this revision to account for the recent SVal simplification commit by @NoQ,

Which commit introduced the regression?

but now there is an exponential blowup problem that prevents testcase PR24184.cpp from terminating,

What triggers the regression? Removing the if statement above? Does the regression only effect the Z3 "mode" (I am guessing not since you said "due to an interaction between Simplifier::VisitNonLocSymbolVal() and SValBuilder::makeSymExprValNN()")?

[ddcc]

lib/StaticAnalyzer/Core/SValBuilder.cpp

357

To clarify, the changes made in this patch aren't specific to Z3 support, especially simplifying SymbolCast and IntSymExpr. With the exception of PR24184.cpp and plist-macros.cpp, all testcases pass with both the default and Z3 constraint managers. However, creating additional constraints does have performance overhead, and it may be useful to consider the parameters for gating this functionality.

On a combined execution (Range + Z3) through the testcases, except the two mentioned above, the runtime is 327 sec with this patch applied, and 195 sec without this patch applied. On a separate execution through the testcases with only the Z3 constraint manager, I get runtimes 320 and 191, respectively.

For testing purposes, I also tried the following code, which has combined runtime 311 sec, but loses the accuracy improvements with the Range constraint manager on bitwise-ops.c, conditional-path-notes.c, explain-svals.cpp, and std-c-library-functions.c.

ConstraintManager &CM = getStateManager().getConstraintManager();
if (!State->isTainted(RHS) && !State->isTainted(LHS) && !CM.isZ3())

364

Reducing the MaxComp is going to regress taint analysis..

I think the original intention was to increase MaxComp, not decrease it, but I will restore the original value here.

What triggers the regression? Removing the if statement above? Does the regression only effect the Z3 "mode"

No, the regression isn't specifically due to this code, but with @NoQ 's patch for SVal simplification (rL300178), and this commit extending it to handle SymbolCast and IntSymExpr, the cast of ST * used in the loop of case 3 of PR24184.cpp becomes "simplified" (inlined) repeatedly on each recursive iteration through Simplifier::VisitNonLocSymbolVal() -> SValBuilder::makeSymExprValNN(), causing a big slowdown in runtime performance.

The naive way to prevent it is to drop MaxComp (but this isn't reasonable, since it needs to be absurdly low, e.g. 10). Alternatively, simplification for SymbolCast can be dropped from this commit (but it will eliminate some of the other analysis improvements), or, most likely, introduce another parameter to reduce recursion between these two functions.

[zaks.anna]

lib/StaticAnalyzer/Core/SValBuilder.cpp

357

Thanks for the explanation!

Regressing the current default behavior is my main concern. By looking at the numbers you provided before (Pre-commit and Post-Commit for RangeConstraintManager), it seems that this patch will introduce a performance regression of about 20%, which is large. But you are pointing out that there are improvements to the modeling as well and those are captured by the updated tests.

Here are a couple of ideas that came into mind on gaining back performance for the RangeConstraintManager case:

• Can we drop computing these for some expressions that we know the RangeConstraintManager will not utilize?
• We could implement the TODO described below and possibly also lower the MaxComp value. This means that instead of keeping a complex expression and constraints on every symbol used in that expression, we would conjure a new symbol and associate a new constrain derived from the expression with it. (Would this strategy also work for the Z3 case?)

I have to point out that this code is currently only used by taint analysis, which is experimental and the current MaxComp value is targeted at that. We would probably need to refine the strategy here if we want to apply this logic to a general case. It's possible that different MaxComp should be used for different cases.

It would be valuable to run this on real code and measure how the number of reports we get differs depending on these values.

[NoQ]

Hmm, curious, having a look. A couple of blind guesses before i actually understand what's going on:

(1) The simplifySVal() code has its own complexity threshold:

1060     SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
1061       // Simplification is much more costly than computing complexity.
1062       // For high complexity, it may be not worth it.
1063       if (V.getSymbol()->computeComplexity() > 100)
1064         return V;
1065       return Visit(V.getSymbol());
1066     }

Would it help to decrease 100 to 10 here?

(2) With RangeConstraintManager, simplification is not entirely idempotent: we may simplify a symbol further when one of its sub-symbols gets constrained to a constant in a new state. However, apart from that, we might be able to avoid re-simplifying the same symbol by caching results based on the (symbol, state's constraint data) pair. Probably it may work with Z3 as well.

[ddcc]

Can we drop computing these for some expressions that we know the RangeConstraintManager will not utilize?

It's possible, though I'm not sure what the actual limitations of the RangeConstraintManager are, since there are a lot of intermediate steps that attempt to transform unsupported expressions into supported ones.

We could implement the TODO described below and possibly also lower the MaxComp value. This means that instead of keeping a complex expression and constraints on every symbol used in that expression, we would conjure a new symbol and associate a new constrain derived from the expression with it. (Would this strategy also work for the Z3 case?)

I think it's feasible, but would probably require some more to code to handle SymbolConjured (right now all SymbolData are treated as variables).

Would it help to decrease 100 to 10 here?

Yes, changing it to 10 eliminates the excessive recursion; combined runtime drops to 282 sec on the testcases (~8 sec for Range only, ~271 sec for Z3 only; doesn't sum due to separate executions). This appears to be the most straightforward solution.

(2) With RangeConstraintManager, simplification is not entirely idempotent: we may simplify a symbol further when one of its sub-symbols gets constrained to a constant in a new state. However, apart from that, we might be able to avoid re-simplifying the same symbol by caching results based on the (symbol, state's constraint data) pair. Probably it may work with Z3 as well.

Yeah, that would also fix this issue. In general, I think there's plenty of room for improvements from caching, especially for queries to e.g. getSymVal().

[ddcc]

Rebase, decrease simplification complexity

[ddcc]

I forgot to mention that the only remaining (Z3) test failure is on plist-macros.cpp; there is a Assuming condition is true path note that only appears with the RangeConstraintManager but not with Z3ConstraintManager, and I can't #ifdef it because the annotations are checked by FileCheck.

[ddcc]

ping

[NoQ]

Because this patch affects the default behavior, i think it's necessary to understand the performance impact on a large codebase. I may lend a hand eventually, but if you're in a hurry you could probably at least run an overnight analysis over llvm and sqlite with range constraint manager and see how performance changes with this patch, and ideally also if we get new reports or lose old reports.

In D28953#785679, @ddcc wrote:

I forgot to mention that the only remaining (Z3) test failure is on plist-macros.cpp; there is a Assuming condition is true path note that only appears with the RangeConstraintManager but not with Z3ConstraintManager, and I can't #ifdef it because the annotations are checked by FileCheck.

This test case could be separated into a different file if nothing else helps.

lib/StaticAnalyzer/Core/SValBuilder.cpp

364

We talked a bit and we're pretty much fine with reduce MaxComp to 10 if it's worth it in terms of performance.

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

997–1003

These two ifs are completely identical (apart from the fact that the one you added ignores symbolic region values due to explicit NonLoc cast). In fact getAsSymbol() (with its optional argument equal to false) and getAsSymExpr() are equivalent; we need to refactor this API.

I believe that the FIXME should in fact be addressed in RangeConstraintManager, in which currently getSymVal() works for atomic symbols only. Or, alternatively, we should stick simplifySVal() here - i think i'd have a look at this soon.

In any case, i suggest removing this change for now, unless i missed anything and it does in fact have an effect.

test/Analysis/plist-macros.cpp

2

path-diagnostics-alternate=ture

Ouch. Thanks for fixing this.

Maybe it'd be great to implement an option that enables validating analyzer config option values, and turn this option on in %clang_analyze_cc1.

[ddcc]

Drop duplicate code

[ddcc]

I tested the following software, both before and after applying this patch, using RangeConstraintManager.

Software, Version, Compile Time (before), Bugs Reported (before), Compile Time (after), Bugs Reported (after)
openssl, 1.1.0f, 11 min, 126, 12 min, 126
sqlite, 3.18.2, 31 min, 86, 31 min, 82
wireshark, 2.2.7, 105 min, 109, 119 min, 108

For sqlite, the differences of four reported bugs all appear to be false positives, but for wireshark, the one difference appears to be a false negative.

lib/StaticAnalyzer/Core/SValBuilder.cpp

364

Just to clarify, the current change from 100 to 10 in simplifySVal::SimplyVisitNonLocSymbolVal resolves the problem; the value of MaxComp here is unchanged.

test/Analysis/plist-macros.cpp

2

I agree that'd be useful, but I think that it should be a separate future patch.

[ddcc]

I've also uploaded the results to https://dcddcc.com/csa

[NoQ]

This looks great, thank you very much.

test/Analysis/plist-macros.cpp

2

Sure sure.

[ddcc]

Split plist-macros.cpp, and update analyzer_test.py to support tests that require not z3

[morehouse]

r307833 is causing the sanitizer-x86_64-linux-fast buildbot to fail during clang regression tests with the following error:

clang: /mnt/b/sanitizer-buildbot3/sanitizer-x86_64-linux-fast/build/llvm/tools/clang/lib/StaticAnalyzer/Core/RangedConstraintManager.cpp:55: virtual clang::ento::ProgramStateRef clang::ento::RangedConstraintManager::assumeSym(clang::ento::ProgramStateRef, clang::ento::SymbolRef, bool): Assertion `Loc::isLocType(SSE->getLHS()->getType())' failed.

Could you please revert and/or fix this revision?

[ddcc]

Reverted in rL307853

[ddcc]

This comment was removed by ddcc.

include/clang/StaticAnalyzer/Checkers/SValExplainer.h

std::string VisitSymIntExpr(const SymIntExpr *S) {
     std::string Str;
     llvm::raw_string_ostream OS(Str);
     OS << "(" << Visit(S->getLHS()) << ") "
        << std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) << " "
        << S->getRHS();
     return OS.str();
   }
 
-  // TODO: IntSymExpr doesn't appear in practice.
-  // Add the relevant code once it does.
+  std::string VisitIntSymExpr(const IntSymExpr *S) {
+    std::string Str;
+    llvm::raw_string_ostream OS(Str);
+    OS << S->getLHS()
+       << std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) << " "
+       << "(" << Visit(S->getRHS()) << ") ";
+    return OS.str();
+  }
 
   std::string VisitSymSymExpr(const SymSymExpr *S) {
     return "(" + Visit(S->getLHS()) + ") " +
            std::string(BinaryOperator::getOpcodeStr(S->getOpcode())) +
            " (" + Visit(S->getRHS()) + ")";
   }
 
-  // TODO: SymbolCast doesn't appear in practice.
-  // Add the relevant code once it does.
+  std::string VisitSymbolCast(const SymbolCast *S) {
+    return "cast of type '" + S->getType().getAsString() + "' of " +
+           Visit(S->getOperand());
+  }
 
   std::string VisitSymbolicRegion(const SymbolicRegion *R) {
     // Explain 'this' object here.
     // TODO: Explain CXXThisRegion itself, find a way to test it.
     if (isThisObject(R))
       return "'this' object";
     // Objective-C objects are not normal symbolic regions. At least,
     // they're always on the heap.

lib/StaticAnalyzer/Core/SValBuilder.cpp

 }
 
 DefinedOrUnknownSVal
 SValBuilder::getRegionValueSymbolVal(const TypedValueRegion* region) {
   QualType T = region->getValueType();
 
   if (T->isNullPtrType())
     return makeZeroVal(T);
-  
   if (!SymbolManager::canSymbolicate(T))
     return UnknownVal();
 
   SymbolRef sym = SymMgr.getRegionValueSymbol(region);
 
   if (Loc::isLocType(T))
     return loc::MemRegionVal(MemMgr.getSymbolicRegion(sym));
 

 }
 
 //===----------------------------------------------------------------------===//
 
 SVal SValBuilder::makeSymExprValNN(ProgramStateRef State,
                                    BinaryOperator::Opcode Op,
                                    NonLoc LHS, NonLoc RHS,
                                    QualType ResultTy) {
-  if (!State->isTainted(RHS) && !State->isTainted(LHS))
-    return UnknownVal();
-
   const SymExpr *symLHS = LHS.getAsSymExpr();
   const SymExpr *symRHS = RHS.getAsSymExpr();
   // TODO: When the Max Complexity is reached, we should conjure a symbol
   // instead of generating an Unknown value and propagate the taint info to it.
   const unsigned MaxComp = 10000; // 100000 28X
 
   if (symLHS && symRHS &&
-      (symLHS->computeComplexity() + symRHS->computeComplexity()) <  MaxComp)
+      (symLHS->computeComplexity() + symRHS->computeComplexity()) < MaxComp)
     return makeNonLoc(symLHS, Op, symRHS, ResultTy);
 
   if (symLHS && symLHS->computeComplexity() < MaxComp)
     if (Optional<nonloc::ConcreteInt> rInt = RHS.getAs<nonloc::ConcreteInt>())
       return makeNonLoc(symLHS, Op, rInt->getValue(), ResultTy);
 
   if (symRHS && symRHS->computeComplexity() < MaxComp)
     if (Optional<nonloc::ConcreteInt> lInt = LHS.getAs<nonloc::ConcreteInt>())

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

case loc::GotoLabelKind:
     // FIXME: we can probably do a comparison against other MemRegions, though.
     // FIXME: is there a way to tell if two labels refer to the same location?
     return UnknownVal();
 
   case loc::ConcreteIntKind: {
     // If one of the operands is a symbol and the other is a constant,
     // build an expression for use by the constraint manager.
     if (SymbolRef rSym = rhs.getAsLocSymbol()) {
-      // We can only build expressions with symbols on the left,
-      // so we need a reversible operator.
+      const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
+
+      // Prefer expressions with symbols on the left
       if (!BinaryOperator::isComparisonOp(op))
-        return UnknownVal();
+        return makeNonLoc(lVal, op, rSym, resultTy);
 
-      const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
       op = BinaryOperator::reverseComparisonOp(op);
       return makeNonLoc(rSym, op, lVal, resultTy);
     }
 
     // If both operands are constants, just perform the operation.
     if (Optional<loc::ConcreteInt> rInt = rhs.getAs<loc::ConcreteInt>()) {
       SVal ResultVal =
           lhs.castAs<loc::ConcreteInt>().evalBinOp(BasicVals, op, *rInt);
if (V.isUnknownOrUndef())
     return nullptr;
 
   if (Optional<loc::ConcreteInt> X = V.getAs<loc::ConcreteInt>())
     return &X->getValue();
 
   if (Optional<nonloc::ConcreteInt> X = V.getAs<nonloc::ConcreteInt>())
     return &X->getValue();
 
   if (SymbolRef Sym = V.getAsSymbol())
     return state->getConstraintManager().getSymVal(state, Sym);
 
-  // FIXME: Add support for SymExprs.
+  if (Optional<NonLoc> NV = V.getAs<NonLoc>())
+    if (SymbolRef Sym = NV->getAsSymExpr())
+      return state->getConstraintManager().getSymVal(state, Sym);
+
   return nullptr;
 }
 
 SVal SimpleSValBuilder::simplifySVal(ProgramStateRef State, SVal V) {
   // For now, this function tries to constant-fold symbols inside a
   // nonloc::SymbolVal, and does nothing else. More simplifications should
   // be possible, such as constant-folding an index in an ElementRegion.
 
   class Simplifier : public FullSValVisitor<Simplifier, SVal> {
     ProgramStateRef State;
     SValBuilder &SVB;
 
   public:
     Simplifier(ProgramStateRef State)
         : State(State), SVB(State->getStateManager().getSValBuilder()) {}
 
     SVal VisitSymbolData(const SymbolData *S) {
       if (const llvm::APSInt *I =
               SVB.getKnownValue(State, nonloc::SymbolVal(S)))
         return Loc::isLocType(S->getType()) ? (SVal)SVB.makeIntLocVal(*I)
                                             : (SVal)SVB.makeIntVal(*I);
       return nonloc::SymbolVal(S);
     }
 
-    // TODO: Support SymbolCast. Support IntSymExpr when/if we actually
-    // start producing them.
+    SVal VisitIntSymExpr(const IntSymExpr *S) {
+      SVal RHS = Visit(S->getRHS());
+      SVal LHS = SVB.makeIntVal(S->getLHS());
+      return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
+    }
 
     SVal VisitSymIntExpr(const SymIntExpr *S) {
       SVal LHS = Visit(S->getLHS());
       SVal RHS;
       // By looking at the APSInt in the right-hand side of S, we cannot
       // figure out if it should be treated as a Loc or as a NonLoc.
       // So make our guess by recalling that we cannot multiply pointers
       // or compare a pointer to an integer.
       if (Loc::isLocType(S->getLHS()->getType()) &&
           BinaryOperator::isComparisonOp(S->getOpcode())) {
         // The usual conversion of $sym to &SymRegion{$sym}, as they have
         // the same meaning for Loc-type symbols, but the latter form
         // is preferred in SVal computations for being Loc itself.
         if (SymbolRef Sym = LHS.getAsSymbol()) {
           assert(Loc::isLocType(Sym->getType()));
           LHS = SVB.makeLoc(Sym);
         }
         RHS = SVB.makeIntLocVal(S->getRHS());
       } else {
         RHS = SVB.makeIntVal(S->getRHS());
       }
       return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
     }
 
+    SVal VisitSymbolCast(const SymbolCast *S) {
+      SVal V = Visit(S->getOperand());
+      return SVB.evalCast(V, S->getType(), S->getOperand()->getType());
+    }
+
     SVal VisitSymSymExpr(const SymSymExpr *S) {
       SVal LHS = Visit(S->getLHS());
       SVal RHS = Visit(S->getRHS());
       return SVB.evalBinOp(State, S->getOpcode(), LHS, RHS, S->getType());
     }
 
     SVal VisitSymExpr(SymbolRef S) { return nonloc::SymbolVal(S); }
 
     SVal VisitMemRegion(const MemRegion *R) { return loc::MemRegionVal(R); }
 
     SVal VisitNonLocSymbolVal(nonloc::SymbolVal V) {
       // Simplification is much more costly than computing complexity.
       // For high complexity, it may be not worth it.
-      if (V.getSymbol()->computeComplexity() > 100)
+      if (V.getSymbol()->computeComplexity() > 10)
         return V;
       return Visit(V.getSymbol());
     }
 
     SVal VisitSVal(SVal V) { return V; }
   };
 
   return Simplifier(State).Visit(V);
 }

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

if (!hasComparison && !RetTy->isBooleanType())
     return assumeZ3Expr(State, Sym, getZ3ZeroExpr(Exp, RetTy, !Assumption));
 
   return assumeZ3Expr(State, Sym, Assumption ? Exp : getZ3NotExpr(Exp));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
+  ASTContext &Ctx = getBasicVals().getContext();
+  // FIXME: This should be a cast from a 1-bit integer type to a boolean type,
+  // but the former is not available in Clang. Instead, extend the APSInt
+  // directly.
+  bool isBoolTy = From.getBitWidth() == 1 && getAPSIntType(From).isNull();
+
   QualType RetTy;
   // The expression may be casted, so we cannot call getZ3DataExpr() directly
   Z3Expr Exp = getZ3Expr(Sym, &RetTy);
-
-  assert((getAPSIntType(From) == getAPSIntType(To)) &&
-         "Range values have different types!");
-  QualType RTy = getAPSIntType(From);
-  bool isSignedTy = RetTy->isSignedIntegerOrEnumerationType();
-  Z3Expr FromExp = Z3Expr::fromAPSInt(From);
-  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+  QualType RTy = isBoolTy ? Ctx.BoolTy : getAPSIntType(From);
+  Z3Expr FromExp =
+      isBoolTy ? Z3Expr::fromAPSInt(From.extend(Ctx.getTypeSize(Ctx.BoolTy)))
+               : Z3Expr::fromAPSInt(From);
 
   // Construct single (in)equality
   if (From == To)
     return assumeZ3Expr(State, Sym,
                         getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
                                      FromExp, RTy, nullptr));
 
+  assert((getAPSIntType(From) == getAPSIntType(To)) &&
+         "Range values have different types!");
+
+  Z3Expr ToExp = Z3Expr::fromAPSInt(To);
   // Construct two (in)equalities, and a logical and/or
   Z3Expr LHS =
       getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
   Z3Expr RHS =
       getZ3BinExpr(Exp, RetTy, InRange ? BO_LE : BO_GT, ToExp, RTy, nullptr);
   return assumeZ3Expr(
       State, Sym,
-      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS, isSignedTy));
+      Z3Expr::fromBinOp(LHS, InRange ? BO_LAnd : BO_LOr, RHS,
+                        RetTy->isSignedIntegerOrEnumerationType()));
 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymUnsupported(ProgramStateRef State,
                                                           SymbolRef Sym,
                                                           bool Assumption) {
   // Skip anything that is unsupported
   return State;
 }
QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
   ASTContext &Ctx = getBasicVals().getContext();
   return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
 }
 
 void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
                                            QualType &LTy, QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Perform type conversion
   if (LTy->isIntegralOrEnumerationType() &&
       RTy->isIntegralOrEnumerationType()) {
     if (LTy->isArithmeticType() && RTy->isArithmeticType())
       return doIntTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
   } else if (LTy->isRealFloatingType() || RTy->isRealFloatingType()) {
     return doFloatTypeConversion<Z3Expr, Z3Expr::fromCast>(LHS, LTy, RHS, RTy);
   } else if ((LTy->isAnyPointerType() || RTy->isAnyPointerType()) ||
void Z3ConstraintManager::doTypeConversion(Z3Expr &LHS, Z3Expr &RHS,
   // TODO: Refine behavior for invalid type casts
 }
 
 template <typename T,
           T(doCast)(const T &, QualType, uint64_t, QualType, uint64_t)>
 void Z3ConstraintManager::doIntTypeConversion(T &LHS, QualType &LTy, T &RHS,
                                               QualType &RTy) const {
   ASTContext &Ctx = getBasicVals().getContext();
-
   uint64_t LBitWidth = Ctx.getTypeSize(LTy);
   uint64_t RBitWidth = Ctx.getTypeSize(RTy);
 
+  assert(!LTy.isNull() && !RTy.isNull() && "Input type is null!");
   // Always perform integer promotion before checking type equality.
   // Otherwise, e.g. (bool) a + (bool) b could trigger a backend assertion
   if (LTy->isPromotableIntegerType()) {
     QualType NewTy = Ctx.getPromotedIntegerType(LTy);
     uint64_t NewBitWidth = Ctx.getTypeSize(NewTy);
     LHS = (*doCast)(LHS, NewTy, NewBitWidth, LTy, LBitWidth);
     LTy = NewTy;
     LBitWidth = NewBitWidth;

test/Analysis/bitwise-ops.c

 // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -triple x86_64-apple-darwin13 -Wno-shift-count-overflow -verify %s
 
 void clang_analyzer_eval(int);
 #define CHECK(expr) if (!(expr)) return; clang_analyzer_eval(expr)
 
 void testPersistentConstraints(int x, int y) {
   // Sanity check
   CHECK(x); // expected-warning{{TRUE}}
   CHECK(x & 1); // expected-warning{{TRUE}}
-  
-  // False positives due to SValBuilder giving up on certain kinds of exprs.
-  CHECK(1 - x); // expected-warning{{UNKNOWN}}
-  CHECK(x & y); // expected-warning{{UNKNOWN}}
+  CHECK(1 - x); // expected-warning{{TRUE}}
+  CHECK(x & y); // expected-warning{{TRUE}}
 }
 
 int testConstantShifts_PR18073(int which) {
   // FIXME: We should have a checker that actually specifically checks bitwise
   // shifts against the width of the LHS's /static/ type, rather than just
   // having BasicValueFactory return "undefined" when dealing with two constant
   // operands.
   switch (which) {
   case 1:
     return 0ULL << 63; // no-warning
   case 2:
     return 0ULL << 64; // expected-warning{{The result of the '<<' expression is undefined}}
   case 3:
     return 0ULL << 65; // expected-warning{{The result of the '<<' expression is undefined}}
 
   default:
     return 0;
   }
-}
+}
 

test/Analysis/bool-assignment.c

 
 void test_BOOL_initialization(int y) {
   BOOL constant = 2; // expected-warning {{Assignment of a non-Boolean value}}
   if (y < 0) {
     BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
     return;
   }
   if (y > 200 && y < 250) {
-#ifdef ANALYZER_CM_Z3
     BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}
-#else
-    BOOL x = y; // no-warning
-#endif
     return;
   }
   if (y >= 127 && y < 150) {
     BOOL x = y; // expected-warning{{Assignment of a non-Boolean value}}
     return;
   }
   if (y > 1) {
     BOOL x = y; // expected-warning {{Assignment of a non-Boolean value}}

test/Analysis/conditional-path-notes.c

if (a && b) {
     // expected-note@-4 {{Taking true branch}}
     *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
     // expected-note@-1 {{Dereference of null pointer}}
   }
 }
 
 void testNonDiagnosableBranchArithmetic(int a, int b) {
   if (a - b) {
-    // expected-note@-1 {{Taking true branch}}
+    // expected-note@-1 {{Assuming the condition is true}}
+    // expected-note@-2 {{Taking true branch}}
     *(volatile int *)0 = 1; // expected-warning{{Dereference of null pointer}}
     // expected-note@-1 {{Dereference of null pointer}}
   }
 }
 
 // CHECK:  <key>diagnostics</key>
 // CHECK-NEXT:  <array>
 // CHECK-NEXT:   <dict>

 // CHECK-NEXT:            <key>line</key><integer>79</integer>
 // CHECK-NEXT:            <key>col</key><integer>4</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:          </array>
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:        </dict>
+// CHECK-NEXT:       </array>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>event</string>
+// CHECK-NEXT:      <key>location</key>
+// CHECK-NEXT:      <dict>
+// CHECK-NEXT:       <key>line</key><integer>79</integer>
+// CHECK-NEXT:       <key>col</key><integer>7</integer>
+// CHECK-NEXT:       <key>file</key><integer>0</integer>
+// CHECK-NEXT:      </dict>
+// CHECK-NEXT:      <key>ranges</key>
+// CHECK-NEXT:      <array>
+// CHECK-NEXT:        <array>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>7</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>79</integer>
+// CHECK-NEXT:          <key>col</key><integer>11</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:        </array>
+// CHECK-NEXT:      </array>
+// CHECK-NEXT:      <key>depth</key><integer>0</integer>
+// CHECK-NEXT:      <key>extended_message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:      <key>message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>control</string>
+// CHECK-NEXT:      <key>edges</key>
+// CHECK-NEXT:       <array>
+// CHECK-NEXT:        <dict>
+// CHECK-NEXT:         <key>start</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>79</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:         <key>end</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:          </array>
 // CHECK-NEXT:        </dict>
 // CHECK-NEXT:       </array>
 // CHECK-NEXT:     </dict>
 // CHECK-NEXT:     <dict>
 // CHECK-NEXT:      <key>kind</key><string>control</string>
 // CHECK-NEXT:      <key>edges</key>
 // CHECK-NEXT:       <array>
 // CHECK-NEXT:        <dict>
 // CHECK-NEXT:         <key>start</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:          </array>
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
-// CHECK-NEXT:            <key>line</key><integer>81</integer>
+// CHECK-NEXT:            <key>line</key><integer>82</integer>
 // CHECK-NEXT:            <key>col</key><integer>24</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:          </array>
 // CHECK-NEXT:        </dict>
 // CHECK-NEXT:       </array>
 // CHECK-NEXT:     </dict>
 // CHECK-NEXT:     <dict>
 // CHECK-NEXT:      <key>kind</key><string>event</string>
 // CHECK-NEXT:      <key>location</key>
 // CHECK-NEXT:      <dict>
-// CHECK-NEXT:       <key>line</key><integer>81</integer>
+// CHECK-NEXT:       <key>line</key><integer>82</integer>
 // CHECK-NEXT:       <key>col</key><integer>24</integer>
 // CHECK-NEXT:       <key>file</key><integer>0</integer>
 // CHECK-NEXT:      </dict>
 // CHECK-NEXT:      <key>ranges</key>
 // CHECK-NEXT:      <array>
 // CHECK-NEXT:        <array>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>5</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
 // CHECK-NEXT:         <dict>
-// CHECK-NEXT:          <key>line</key><integer>81</integer>
+// CHECK-NEXT:          <key>line</key><integer>82</integer>
 // CHECK-NEXT:          <key>col</key><integer>26</integer>
 // CHECK-NEXT:          <key>file</key><integer>0</integer>
 // CHECK-NEXT:         </dict>
 // CHECK-NEXT:        </array>
 // CHECK-NEXT:      </array>
 // CHECK-NEXT:      <key>depth</key><integer>0</integer>
 // CHECK-NEXT:      <key>extended_message</key>
 // CHECK-NEXT:      <string>Dereference of null pointer</string>
 // CHECK-NEXT:      <key>message</key>
 // CHECK-NEXT:      <string>Dereference of null pointer</string>
 // CHECK-NEXT:     </dict>
 // CHECK-NEXT:    </array>
 // CHECK-NEXT:    <key>description</key><string>Dereference of null pointer</string>
 // CHECK-NEXT:    <key>category</key><string>Logic error</string>
 // CHECK-NEXT:    <key>type</key><string>Dereference of null pointer</string>
 // CHECK-NEXT:    <key>check_name</key><string>core.NullDereference</string>
 // CHECK-NEXT:    <!-- This hash is experimental and going to change! -->
 // CHECK-NEXT:    <key>issue_hash_content_of_line_in_context</key><string>f56671e5f67c73abef619b56f7c29fa4</string>
 // CHECK-NEXT:   <key>issue_context_kind</key><string>function</string>
 // CHECK-NEXT:   <key>issue_context</key><string>testNonDiagnosableBranchArithmetic</string>
-// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>3</string>
+// CHECK-NEXT:   <key>issue_hash_function_offset</key><string>4</string>
 // CHECK-NEXT:   <key>location</key>
 // CHECK-NEXT:   <dict>
-// CHECK-NEXT:    <key>line</key><integer>81</integer>
+// CHECK-NEXT:    <key>line</key><integer>82</integer>
 // CHECK-NEXT:    <key>col</key><integer>24</integer>
 // CHECK-NEXT:    <key>file</key><integer>0</integer>
 // CHECK-NEXT:   </dict>
 // CHECK-NEXT:   </dict>
 // CHECK-NEXT:  </array>

test/Analysis/explain-svals.cpp

void test_3(S s) {
   }
 }
 
 void test_4(int x, int y) {
   int z;
   static int stat;
   clang_analyzer_explain(x + 1); // expected-warning-re{{{{^\(argument 'x'\) \+ 1$}}}}
   clang_analyzer_explain(1 + y); // expected-warning-re{{{{^\(argument 'y'\) \+ 1$}}}}
-  clang_analyzer_explain(x + y); // expected-warning-re{{{{^unknown value$}}}}
+  clang_analyzer_explain(x + y); // expected-warning-re{{{{^\(argument 'x'\) \+ \(argument 'y'\)$}}}}
   clang_analyzer_explain(z); // expected-warning-re{{{{^undefined value$}}}}
   clang_analyzer_explain(&z); // expected-warning-re{{{{^pointer to local variable 'z'$}}}}
   clang_analyzer_explain(stat); // expected-warning-re{{{{^signed 32-bit integer '0'$}}}}
   clang_analyzer_explain(&stat); // expected-warning-re{{{{^pointer to static local variable 'stat'$}}}}
   clang_analyzer_explain(stat_glob); // expected-warning-re{{{{^initial value of global variable 'stat_glob'$}}}}
   clang_analyzer_explain(&stat_glob); // expected-warning-re{{{{^pointer to global variable 'stat_glob'$}}}}
   clang_analyzer_explain((int[]){1, 2, 3}); // expected-warning-re{{{{^pointer to element of type 'int' with index 0 of temporary object constructed at statement '\(int \[3\]\)\{1, 2, 3\}'$}}}}
 }

test/Analysis/plist-macros.cpp

 // RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=ture %s -o %t.plist
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-eagerly-assume -analyzer-output=plist-multi-file -analyzer-config path-diagnostics-alternate=true %s -o %t.plist
 // RUN: FileCheck --input-file=%t.plist %s
 
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
 
 #define mallocmemory int *x = (int*)malloc(12);
 void noteOnMacro(int y) {

 
 void test1() {
   CALL_FN(0);
 }
 
 void test2(int *p) {
   CALL_FN(p);
 }
+
 // CHECK:  <key>diagnostics</key>
 // CHECK-NEXT:  <array>
 // CHECK-NEXT:   <dict>
 // CHECK-NEXT:    <key>path</key>
 // CHECK-NEXT:    <array>
 // CHECK-NEXT:     <dict>
 // CHECK-NEXT:      <key>kind</key><string>control</string>
 // CHECK-NEXT:      <key>edges</key>

 // CHECK-NEXT:            <key>line</key><integer>36</integer>
 // CHECK-NEXT:            <key>col</key><integer>4</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:          </array>
 // CHECK-NEXT:         <key>end</key>
 // CHECK-NEXT:          <array>
 // CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:        </dict>
+// CHECK-NEXT:       </array>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>event</string>
+// CHECK-NEXT:      <key>location</key>
+// CHECK-NEXT:      <dict>
+// CHECK-NEXT:       <key>line</key><integer>36</integer>
+// CHECK-NEXT:       <key>col</key><integer>7</integer>
+// CHECK-NEXT:       <key>file</key><integer>0</integer>
+// CHECK-NEXT:      </dict>
+// CHECK-NEXT:      <key>ranges</key>
+// CHECK-NEXT:      <array>
+// CHECK-NEXT:        <array>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>36</integer>
+// CHECK-NEXT:          <key>col</key><integer>7</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:         <dict>
+// CHECK-NEXT:          <key>line</key><integer>36</integer>
+// CHECK-NEXT:          <key>col</key><integer>25</integer>
+// CHECK-NEXT:          <key>file</key><integer>0</integer>
+// CHECK-NEXT:         </dict>
+// CHECK-NEXT:        </array>
+// CHECK-NEXT:      </array>
+// CHECK-NEXT:      <key>depth</key><integer>0</integer>
+// CHECK-NEXT:      <key>extended_message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:      <key>message</key>
+// CHECK-NEXT:      <string>Assuming the condition is true</string>
+// CHECK-NEXT:     </dict>
+// CHECK-NEXT:     <dict>
+// CHECK-NEXT:      <key>kind</key><string>control</string>
+// CHECK-NEXT:      <key>edges</key>
+// CHECK-NEXT:       <array>
+// CHECK-NEXT:        <dict>
+// CHECK-NEXT:         <key>start</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:           <dict>
+// CHECK-NEXT:            <key>line</key><integer>36</integer>
+// CHECK-NEXT:            <key>col</key><integer>7</integer>
+// CHECK-NEXT:            <key>file</key><integer>0</integer>
+// CHECK-NEXT:           </dict>
+// CHECK-NEXT:          </array>
+// CHECK-NEXT:         <key>end</key>
+// CHECK-NEXT:          <array>
+// CHECK-NEXT:           <dict>
 // CHECK-NEXT:            <key>line</key><integer>37</integer>
 // CHECK-NEXT:            <key>col</key><integer>5</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>
 // CHECK-NEXT:           </dict>
 // CHECK-NEXT:           <dict>
 // CHECK-NEXT:            <key>line</key><integer>37</integer>
 // CHECK-NEXT:            <key>col</key><integer>6</integer>
 // CHECK-NEXT:            <key>file</key><integer>0</integer>

test/Analysis/range_casts.c

void f6(long foo)
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f7(long foo)
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1 == 0) // Was not reached prior fix.
-    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1 == 0)
+    clang_analyzer_warnIfReached(); // no-warning
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f8(long foo)
 {
   unsigned index = -1;
   if (index < foo) index = foo;
   if (index + 1L == 0L)
     clang_analyzer_warnIfReached(); // no-warning
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f9(long foo)
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1L == 0L) // Was not reached prior fix.
-    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1L == 0L)
+    clang_analyzer_warnIfReached(); // no-warning
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f10(long foo)
 {
   unsigned index = -1;
   if (index < foo) index = foo;
void f11(long foo)
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f12(long foo)
 {
   unsigned index = -1;
   if (index < foo) index = foo;
-  if (index - 1UL == 0L) // Was not reached prior fix.
-    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
+  if (index - 1UL == 0L)
+    clang_analyzer_warnIfReached(); // no-warning
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f13(int foo)
 {
   unsigned short index = -1;
   if (index < foo) index = foo;

test/Analysis/std-c-library-functions.c

 size_t fread(void *, size_t, size_t, FILE *);
 size_t fwrite(const void *restrict, size_t, size_t, FILE *restrict);
 void test_fread_fwrite(FILE *fp, int *buf) {
   size_t x = fwrite(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(x <= 10); // expected-warning{{TRUE}}
   size_t y = fread(buf, sizeof(int), 10, fp);
   clang_analyzer_eval(y <= 10); // expected-warning{{TRUE}}
   size_t z = fwrite(buf, sizeof(int), y, fp);
-  // FIXME: should be TRUE once symbol-symbol constraint support is improved.
-  clang_analyzer_eval(z <= y); // expected-warning{{UNKNOWN}}
+  clang_analyzer_eval(z <= y); // expected-warning{{TRUE}}
 }
 
 ssize_t getline(char **, size_t *, FILE *);
 void test_getline(FILE *fp) {
   char *line = 0;
   size_t n = 0;
   ssize_t len;
   while ((len = getline(&line, &n, fp)) != -1) {