[analyzer] Support generating and reasoning over more symbolic constraint types

[ddcc]

Summary

Generate more IntSymExpr constraints, perform SVal simplification for IntSymExpr and SymbolCast constraints, and create fully symbolic SymExprs. Also fixes crashes and adds support for tests that should not be run with Z3ConstraintManager.

[ddcc]

Modify Z3RangeConstraintManager::fixAPSInt() and add Expr::isCommutativeOp()

[ddcc]

Compared with D28953, this revision fixes the test failure with PR3991.m with RangeConstraintManager, and a few other failures with Z3ConstraintManager. However, there's one remaining test failure in range_casts.c that I'm not sure how to resolve. For reference, this is the simplified code snippet from that testcase:

void f15(long foo) {
  unsigned index = -1;
  if (index < foo) index = foo;
  unsigned int tmp = index + 1;
  if (tmp == 0)
    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
  else
    clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
}

In debug mode, an assertion about the system being over-constrained is thrown from ConstraintManager.h. This is because the new Simplifier::VisitSymbolCast function will attempt to evaluate the cast (unsigned int) (reg_$0<long foo>), which is suppressed by the call to haveSameType() in SimpleSValBuilder::evalCastFromNonLoc (D28955 fixes this, but only for Z3ConstraintManager), generating just the symbol reg_$0<long foo>. Subsequently, the analyzer will attempt to evaluate the expression ((reg_$0<long foo>) + 1U) == 0U with the range reg_$0<long foo> : { [4294967296, 9223372036854775807] }, or [UINT_MAX + 1, LONG_MAX]. However, in the case where the assumption is true, RangeConstraintManager takes the intersection of the previous range with [UINT_MAX, UINT_MAX] and produces the empty set, and likewise where the assumption is false, the intersection with [UINT_MAX - 1, 0] again produces the empty set. As a result, both program states are NULL, triggering the assertion.

I'm now somewhat inclined to drop the addition of Simplified::VisitSymbolCast() and those associated testsuite changes, because ignoring type casts is clearly incorrect and will introduce both false negatives and false positives.

[NoQ]

I'd have a look soon.

Is diff 1 the original diff from D28953? It was ok to reopen it, but the new revision is also fine.

Regarding 1-bit bools: did you notice D32328 and D35041, do they accidentally help?

include/clang/AST/Expr.h

3107

There seems to be a typo somewhere around the last comparison.

[ddcc]

Fix typo

[ddcc]

Is diff 1 the original diff from D28953? It was ok to reopen it, but the new revision is also fine.

No, diff 1 is already different; it contains most of the bugfixes. I couldn't find any way to reopen the previous review, and arc diff wouldn't let me update a closed review.

Regarding 1-bit bools: did you notice D32328 and D35041, do they accidentally help?

I did see those changes, but I think they're a little different. The test failures I ran into were cases where the input is a 1-bit APSInt, and attempting to retrieve the type for that gives a null QualType.

[ddcc]

Fix tests after typo fix

[ddcc]

As an update, after fixing the typo and updating the tests, the assertion in range_casts.c is no longer triggered and everything seems fine now.

[ddcc]

Minor style fix

[ddcc]

@NoQ ping

[zaks.anna]

lib/StaticAnalyzer/Core/SValBuilder.cpp

370

As a follow up to the previous version of this patch, I do not think we should set the default complexity limit to 10000.

What is the relation between this limit and the limit in VisitNonLocSymbolVal? If they are related, would it be worthwhile turning these into an analyzer option?

[ddcc]

lib/StaticAnalyzer/Core/SValBuilder.cpp

370

To clarify, the current version of this patch does not modify the MaxComp parameter.

My understanding is that MaxComp is the upper bound for building a new NonLoc symbol from two children, based on the sum of the number of child symbols (complexity) across both children.

In contrast, the limit in VisitNonLocSymbolVal (@NoQ, correct me if I'm wrong), is the upper bound for recursively evaluating and inlining a NonLoc symbol, triggered from simplifySVal by evalBinOpNN. Note that these two latter functions indirectly call each other recursively (through evalBinOp), causing the previous runtime blowup. Furthermore, each call to computeComplexitywill re-iterate through all child symbols of the current symbol, but only the first complexity check at the root symbol is actually necessary, because by definition the complexity of a child symbol at each recursive call is monotonically decreasing.

I think it'd be useful to allow both to be configurable, but I don't see a direct relationship between the two.

[zaks.anna]

lib/StaticAnalyzer/Core/SValBuilder.cpp

370

To clarify, the current version of this patch does not modify the MaxComp parameter.

I know. Also, currently, it is only used in the unsupported taint tracking mode and only for tainted symbols. I would like a different smaller default for all expressions.

[ddcc]

lib/StaticAnalyzer/Core/SValBuilder.cpp

370

Ok. I can make both configurable as part of this patch, with a new default of 10 for VisitNonLocSymbolVal. But I've never used the taint tracking mode, so I don't know what would be a reasonable default for MaxComp.

[zaks.anna]

But I've never used the taint tracking mode, so I don't know what would be a reasonable default for MaxComp.

that one is very experimental anyway. I'd just keep the functional changes to tain out of this patch and use the current default that taint uses.

[ddcc]

Rebase, make complexity limits configurable

[ddcc]

All testcases pass, except the issue with range_casts.c. The cause is still the range intersection discussed in https://reviews.llvm.org/D35450#810469.

[george.karpenkov]

@ddcc Hi, are you still interested in landing the fixes associated with this patch? I can take a look as I'm currently reviewing https://reviews.llvm.org/D45517, but it is likely that the patch would need to be changed substantially before it could land.

[ddcc]

In D35450#1116535, @george.karpenkov wrote:

@ddcc Hi, are you still interested in landing the fixes associated with this patch? I can take a look as I'm currently reviewing https://reviews.llvm.org/D45517, but it is likely that the patch would need to be changed substantially before it could land.

@george.karpenkov Yeah, I've got this and a couple of other patches still awaiting review. If it's easier, I can also split out the APSInt fix into a separate patch.

[george.karpenkov]

I can also split out the APSInt fix into a separate patch.

Yes please.

In general I really dislike arbitrary "complexity cutoffs", as they make further debugging hard and may lead to weird bugs: could you explain why is that required and can not be avoided?

[george.karpenkov]

@ddcc so would be great if we could split this patch into smaller chunks.

include/clang/AST/Expr.h

 
 public:
   OpaqueValueExpr(SourceLocation Loc, QualType T, ExprValueKind VK,
                   ExprObjectKind OK = OK_Ordinary,
                   Expr *SourceExpr = nullptr)
     : Expr(OpaqueValueExprClass, T, VK, OK,
            T->isDependentType() ||
            (SourceExpr && SourceExpr->isTypeDependent()),
-           T->isDependentType() || 
+           T->isDependentType() ||
            (SourceExpr && SourceExpr->isValueDependent()),
            T->isInstantiationDependentType() ||
            (SourceExpr && SourceExpr->isInstantiationDependent()),
            false),
       SourceExpr(SourceExpr), Loc(Loc) {
   }
 
   /// Given an expression which invokes a copy constructor --- i.e.  a
public:
   static bool isLogicalOp(Opcode Opc) { return Opc == BO_LAnd || Opc==BO_LOr; }
   bool isLogicalOp() const { return isLogicalOp(getOpcode()); }
 
   static bool isAssignmentOp(Opcode Opc) {
     return Opc >= BO_Assign && Opc <= BO_OrAssign;
   }
   bool isAssignmentOp() const { return isAssignmentOp(getOpcode()); }
 
+  static bool isCommutativeOp(Opcode Opc) {
+    return Opc == BO_Mul || Opc == BO_Add || (Opc >= BO_EQ && Opc <= BO_Or);
+  }
+  bool isCommutativeOp() const {
+    return isCommutativeOp(getOpcode());
+  }
+
   static bool isCompoundAssignmentOp(Opcode Opc) {
     return Opc > BO_Assign && Opc <= BO_OrAssign;
   }
   bool isCompoundAssignmentOp() const {
     return isCompoundAssignmentOp(getOpcode());
   }
   static Opcode getOpForCompoundAssignment(Opcode Opc) {
     assert(isCompoundAssignmentOp(Opc));
child_range children() {
     return child_range(child_iterator(), child_iterator());
   }
   const_child_range children() const {
     return const_child_range(const_child_iterator(), const_child_iterator());
   }
 
   SourceLocation getLocStart() const LLVM_READONLY { return SourceLocation(); }
   SourceLocation getLocEnd() const LLVM_READONLY { return SourceLocation(); }
-  
   static bool classof(const Stmt *T) {
     return T->getStmtClass() == TypoExprClass;
   }
 
 };
 } // end namespace clang
 
 #endif // LLVM_CLANG_AST_EXPR_H

include/clang/Config/config.h.cmake

 #define DEFAULT_SYSROOT "${DEFAULT_SYSROOT}"
 
 /* Directory where gcc is installed. */
 #define GCC_INSTALL_PREFIX "${GCC_INSTALL_PREFIX}"
 
 /* Define if we have libxml2 */
 #cmakedefine CLANG_HAVE_LIBXML ${CLANG_HAVE_LIBXML}
 
-/* Define if we have z3 and want to build it */
+/* Define if we have z3 and want to build with it */
 #cmakedefine CLANG_ANALYZER_WITH_Z3 ${CLANG_ANALYZER_WITH_Z3}
 
 /* Define if we have sys/resource.h (rlimits) */
 #cmakedefine CLANG_HAVE_RLIMITS ${CLANG_HAVE_RLIMITS}
 
 /* The LLVM product name and version */
 #define BACKEND_PACKAGE_STRING "${BACKEND_PACKAGE_STRING}"
 

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.

include/clang/StaticAnalyzer/Core/AnalyzerOptions.h

private:
   Optional<bool> ReportIssuesInMainSourceFile;
 
   /// \sa StableReportFilename
   Optional<bool> StableReportFilename;
 
   /// \sa getGraphTrimInterval
   Optional<unsigned> GraphTrimInterval;
 
+  /// \sa getMaxSimplifyComplexity
+  Optional<unsigned> MaxSimplifyComplexity;
+
+  /// \sa getMaxTaintComplexity
+  Optional<unsigned> MaxTaintComplexity;
+
   /// \sa getMaxTimesInlineLarge
   Optional<unsigned> MaxTimesInlineLarge;
 
   /// \sa getMinCFGSizeTreatFunctionsAsLarge
   Optional<unsigned> MinCFGSizeTreatFunctionsAsLarge;
 
   /// \sa getMaxNodesPerTopLevelFunction
   Optional<unsigned> MaxNodesPerTopLevelFunction;
public:
 
   /// Returns how often nodes in the ExplodedGraph should be recycled to save
   /// memory.
   ///
   /// This is controlled by the 'graph-trim-interval' config option. To disable
   /// node reclamation, set the option to "0".
   unsigned getGraphTrimInterval();
 
+  /// Returns the maximum complexity of symbolic constraint to generate
+  /// when taint analysis checkers are enabled (10000 by default).
+  ///
+  /// This is controlled by "-analyzer-config max-simplify-complexity" option.
+  unsigned getMaxSimplifyComplexity();
+
+  /// Returns the maximum complexity of symbolic constraints to simplify
+  /// through recursive evaluation (10 by default).
+  ///
+  /// This is controlled by "-analyzer-config max-taint-complexity" option.
+  unsigned getMaxTaintComplexity();
+
   /// Returns the maximum times a large function could be inlined.
   ///
   /// This is controlled by the 'max-times-inline-large' config option.
   unsigned getMaxTimesInlineLarge();
 
   /// Returns the number of basic blocks a function needs to have to be
   /// considered large for the 'max-times-inline-large' config option.
   ///

include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h

ProgramStatePair assumeDual(ProgramStateRef State, DefinedSVal Cond) {
     if (!StTrue) {
 #ifndef __OPTIMIZE__
       // This check is expensive and should be disabled even in Release+Asserts
       // builds.
       // FIXME: __OPTIMIZE__ is a GNU extension that Clang implements but MSVC
       // does not. Is there a good equivalent there?
       assert(assume(State, Cond, false) && "System is over constrained.");
 #endif
-      return ProgramStatePair((ProgramStateRef)nullptr, State);
+      return ProgramStatePair((ProgramStateRef) nullptr, State);
     }
 
     ProgramStateRef StFalse = assume(State, Cond, false);
     if (!StFalse) {
       // We are careful to return the original state, /not/ StTrue,
       // because we want to avoid having callers generate a new node
       // in the ExplodedGraph.
       return ProgramStatePair(State, (ProgramStateRef)nullptr);

lib/StaticAnalyzer/Core/AnalyzerOptions.cpp

 }
 
 unsigned AnalyzerOptions::getGraphTrimInterval() {
   if (!GraphTrimInterval.hasValue())
     GraphTrimInterval = getOptionAsInteger("graph-trim-interval", 1000);
   return GraphTrimInterval.getValue();
 }
 
+unsigned AnalyzerOptions::getMaxSimplifyComplexity() {
+  if (!MaxSimplifyComplexity.hasValue())
+    MaxSimplifyComplexity = getOptionAsInteger("max-simplify-complexity", 10);
+  return MaxSimplifyComplexity.getValue();
+}
+
+unsigned AnalyzerOptions::getMaxTaintComplexity() {
+  if (!MaxTaintComplexity.hasValue())
+    MaxTaintComplexity = getOptionAsInteger("max-taint-complexity", 10000);
+  return MaxTaintComplexity.getValue();
+}
+
 unsigned AnalyzerOptions::getMaxTimesInlineLarge() {
   if (!MaxTimesInlineLarge.hasValue())
     MaxTimesInlineLarge = getOptionAsInteger("max-times-inline-large", 32);
   return MaxTimesInlineLarge.getValue();
 }
 
 unsigned AnalyzerOptions::getMinCFGSizeTreatFunctionsAsLarge() {
   if (!MinCFGSizeTreatFunctionsAsLarge.hasValue())

lib/StaticAnalyzer/Core/RangeConstraintManager.cpp

 
 std::unique_ptr<ConstraintManager>
 ento::CreateRangeConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
   return llvm::make_unique<RangeConstraintManager>(Eng, StMgr.getSValBuilder());
 }
 
 bool RangeConstraintManager::canReasonAbout(SVal X) const {
   Optional<nonloc::SymbolVal> SymVal = X.getAs<nonloc::SymbolVal>();
-  if (SymVal && SymVal->isExpression()) {
-    const SymExpr *SE = SymVal->getSymbol();
+  if (!SymVal)
+    return true;
+
+  do {
+    if (isa<SymbolData>(SE)) {
+      return true;
+    }
 
-    if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(SE)) {
-      switch (SIE->getOpcode()) {
-      // We don't reason yet about bitwise-constraints on symbolic values.
-      case BO_And:
-      case BO_Or:
-      case BO_Xor:
+    if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(SE)) {
+      BinaryOperator::Opcode Op = BSE->getOpcode();
+
+      if (isa<IntSymExpr>(BSE)) {
         return false;
-      // We don't reason yet about these arithmetic constraints on
-      // symbolic values.
-      case BO_Mul:
-      case BO_Div:
-      case BO_Rem:
-      case BO_Shl:
-      case BO_Shr:
+      }
+
+      if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
+        if (BinaryOperator::isMultiplicativeOp(Op) ||
+            BinaryOperator::isShiftOp(Op) || BinaryOperator::isBitwiseOp(Op)) {
+          // We don't reason yet about bitwise-constraints on symbolic values.
+          // We don't reason yet about arithmetic constraints on symbolic values
           return false;
-      // All other cases.
-      default:
-        return true;
         }
+
+        // The simplification case of RangedConstraintManager::assumeSymRel()
+        if (isa<BinarySymExpr>(SIE->getLHS()) &&
+            BinaryOperator::isEqualityOp(Op) && SIE->getRHS() == 0 &&
+            BinaryOperator::isComparisonOp(
+                cast<BinarySymExpr>(SIE->getLHS())->getOpcode())) {
+          SE = SIE->getLHS();
+          continue;
         }
 
-    if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(SE)) {
-      if (BinaryOperator::isComparisonOp(SSE->getOpcode())) {
-        // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
-        if (Loc::isLocType(SSE->getLHS()->getType())) {
-          assert(Loc::isLocType(SSE->getRHS()->getType()));
-          return true;
-        }
+
+      if (const SymSymExpr *SSE = dyn_cast<SymSymExpr>(BSE)) {
+        if (!BinaryOperator::isComparisonOp(Op) ||
+            !Loc::isLocType(SSE->getLHS()->getType()) ||
+            !Loc::isLocType(SSE->getRHS()->getType())) {
+          // We handle Loc <> Loc comparisons, but not (yet) NonLoc <> NonLoc.
+          return false;
+        }
+
+        return canReasonAbout(nonloc::SymbolVal(SSE->getLHS())) &&
+               canReasonAbout(nonloc::SymbolVal(SSE->getRHS()));
       }
     }
 
     return false;
-  }
+  } while (SE);
 
   return true;
 }
 
 ConditionTruthVal RangeConstraintManager::checkNull(ProgramStateRef State,
                                                     SymbolRef Sym) {
   const RangeSet *Ranges = State->get<ConstraintRange>(Sym);
 

lib/StaticAnalyzer/Core/RangedConstraintManager.cpp

ProgramStateRef RangedConstraintManager::assumeSymRel(ProgramStateRef State,
 
   // Simplification: translate an assume of a constraint of the form
   // "(exp comparison_op expr) != 0" to true into an assume of
   // "exp comparison_op expr" to true. (And similarly, an assume of the form
   // "(exp comparison_op expr) == 0" to true into an assume of
   // "exp comparison_op expr" to false.)
   if (Int == 0 && (Op == BO_EQ || Op == BO_NE)) {
     if (const BinarySymExpr *SE = dyn_cast<BinarySymExpr>(Sym))
-      if (BinaryOperator::isComparisonOp(SE->getOpcode()))
+      if (BinaryOperator::isComparisonOp(SE->getOpcode())) {
         return assumeSym(State, Sym, (Op == BO_NE ? true : false));
       }
+  }
 
   // Get the type used for calculating wraparound.
   BasicValueFactory &BVF = getBasicVals();
   APSIntType WraparoundType = BVF.getAPSIntType(Sym->getType());
 
   // We only handle simple comparisons of the form "$sym == constant"
   // or "($sym+constant1) == constant2".
   // The adjustment is "constant1" in the above expression. It's used to

lib/StaticAnalyzer/Core/SValBuilder.cpp

 //  This file defines SValBuilder, the base class for all (complete) SValBuilder
 //  implementations.
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/AST/DeclCXX.h"
 #include "clang/AST/ExprCXX.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/BasicValueFactory.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
 
 using namespace clang;
 using namespace ento;
 
 //===----------------------------------------------------------------------===//
 // Basic SVal creation.
 //===----------------------------------------------------------------------===//
 

 }
 
 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
+
+  AnalyzerOptions &Opts =
+      StateMgr.getOwningEngine()->getAnalysisManager().options;
+  const unsigned MaxComp = Opts.getMaxTaintComplexity(); // 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>())
       return makeNonLoc(lInt->getValue(), Op, symRHS, ResultTy);
 
   return UnknownVal();
 }
 
-
 SVal SValBuilder::evalBinOp(ProgramStateRef state, BinaryOperator::Opcode op,
                             SVal lhs, SVal rhs, QualType type) {
 
   if (lhs.isUndef() || rhs.isUndef())
     return UndefinedVal();
 
   if (lhs.isUnknown() || rhs.isUnknown())
     return UnknownVal();

lib/StaticAnalyzer/Core/SimpleSValBuilder.cpp

 // SimpleSValBuilder.cpp - A basic SValBuilder -----------------------*- C++ -*-
 //
 //                     The LLVM Compiler Infrastructure
 //
 // This file is distributed under the University of Illinois Open Source
 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
 //
 //  This file defines SimpleSValBuilder, a basic implementation of SValBuilder.
 //
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValVisitor.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
 
 using namespace clang;
 using namespace ento;
 
 namespace {
 class SimpleSValBuilder : public SValBuilder {
 protected:
   SVal dispatchCast(SVal val, QualType castTy) override;
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.
-      if (!BinaryOperator::isComparisonOp(op))
-        return UnknownVal();
-
       const llvm::APSInt &lVal = lhs.castAs<loc::ConcreteInt>().getValue();
-      op = BinaryOperator::reverseComparisonOp(op);
+
+      if (BinaryOperator::isCommutativeOp(op))
         return makeNonLoc(rSym, op, lVal, resultTy);
+
+      if (BinaryOperator::isComparisonOp(op)) {
+        BinaryOperator::Opcode NewOp = BinaryOperator::reverseComparisonOp(op);
+        return makeNonLoc(rSym, NewOp, lVal, resultTy);
+      }
+
+      // Prefer expressions with symbols on the left
+      return makeNonLoc(lVal, op, rSym, 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 (Optional<NonLoc> Result = ResultVal.getAs<NonLoc>())
         return evalCastFromNonLoc(*Result, resultTy);
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.
+  // FIXME: Add support for SymExprs in RangeConstraintManager.
+
   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;
+    AnalyzerOptions &Opts;
 
   public:
     Simplifier(ProgramStateRef State)
-        : State(State), SVB(State->getStateManager().getSValBuilder()) {}
+        : State(State), SVB(State->getStateManager().getSValBuilder()),
+          Opts(State->getStateManager()
+                   .getOwningEngine()
+                   ->getAnalysisManager()
+                   .options) {}
 
     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 Loc::isLocType(S->getType()) ? (SVal)SVB.makeLoc(S) 
+      return Loc::isLocType(S->getType()) ? (SVal)SVB.makeLoc(S)
                                           : 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)
+      // Use a lower bound to avoid recursive blowup, e.g. on PR24184.cpp
+
+      // FIXME: Complexity monotonically decreases in child recursive calls,
+      // avoid calling this repeatedly
+      if (V.getSymbol()->computeComplexity() > Opts.getMaxSimplifyComplexity())
         return V;
       return Visit(V.getSymbol());
     }
 
     SVal VisitSVal(SVal V) { return V; }
   };
 
   return Simplifier(State).Visit(V);
 }

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

private:
   //===------------------------------------------------------------------===//
   // Helper functions.
   //===------------------------------------------------------------------===//
 
   // Recover the QualType of an APSInt.
   // TODO: Refactor to put elsewhere
   QualType getAPSIntType(const llvm::APSInt &Int) const;
 
+  // Fix the input APSInt if it is has a bitwidth of 1, and set the type.
+  const llvm::APSInt &fixAPSInt(const llvm::APSInt &Int, llvm::APSInt &NewInt,
+                                QualType *Ty = nullptr) const;
+
   // Perform implicit type conversion on binary symbolic expressions.
   // May modify all input parameters.
   // TODO: Refactor to use built-in conversion functions
   void doTypeConversion(Z3Expr &LHS, Z3Expr &RHS, QualType &LTy,
                         QualType &RTy) const;
 
   // Perform implicit integer type conversion.
   // May modify all input parameters.

 }
 
 ProgramStateRef Z3ConstraintManager::assumeSymInclusiveRange(
     ProgramStateRef State, SymbolRef Sym, const llvm::APSInt &From,
     const llvm::APSInt &To, bool InRange) {
   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 LTy;
+  llvm::APSInt NewFromInt;
+  Z3Expr FromExp = Z3Expr::fromAPSInt(fixAPSInt(From, NewFromInt, &LTy));
 
   // Construct single (in)equality
   if (From == To)
     return assumeZ3Expr(State, Sym,
                         getZ3BinExpr(Exp, RetTy, InRange ? BO_EQ : BO_NE,
-                                     FromExp, RTy, nullptr));
+                                     FromExp, LTy, nullptr));
 
+  QualType RTy;
+  llvm::APSInt NewToInt;
+  Z3Expr ToExp = Z3Expr::fromAPSInt(fixAPSInt(To, NewToInt, &RTy));
+  assert(LTy == RTy && "Range values have different types!");
   // Construct two (in)equalities, and a logical and/or
   Z3Expr LHS =
-      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, RTy, nullptr);
+      getZ3BinExpr(Exp, RetTy, InRange ? BO_GE : BO_LT, FromExp, LTy, 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;
 }
else if (isSat == Z3_L_FALSE && isNotSat == Z3_L_TRUE)
     return false;
 
   // Zero may be a solution
   return ConditionTruthVal();
 }
 
 const llvm::APSInt *Z3ConstraintManager::getSymVal(ProgramStateRef State,
                                                    SymbolRef Sym) const {
-  BasicValueFactory &BV = getBasicVals();
-  ASTContext &Ctx = BV.getContext();
+  BasicValueFactory &BVF = getBasicVals();
+  ASTContext &Ctx = BVF.getContext();
 
   if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
     QualType Ty = Sym->getType();
     assert(!Ty->isRealFloatingType());
     llvm::APSInt Value(Ctx.getTypeSize(Ty),
                        !Ty->isSignedIntegerOrEnumerationType());
 
     Z3Expr Exp = getZ3DataExpr(SD->getSymbolID(), Ty);
Z3Expr NotExp = Z3Expr::fromBinOp(
                             : Z3Expr::fromAPSInt(Value),
         false);
 
     Solver.addConstraint(NotExp);
     if (Solver.check() == Z3_L_TRUE)
       return nullptr;
 
     // This is the only solution, store it
-    return &BV.getValue(Value);
+    return &BVF.getValue(Value);
   } else if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
     SymbolRef CastSym = SC->getOperand();
     QualType CastTy = SC->getType();
     // Skip the void type
     if (CastTy->isVoidType())
       return nullptr;
 
     const llvm::APSInt *Value;
     if (!(Value = getSymVal(State, CastSym)))
       return nullptr;
-    return &BV.Convert(SC->getType(), *Value);
+    return &BVF.Convert(SC->getType(), *Value);
   } else if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
     const llvm::APSInt *LHS, *RHS;
     if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
       LHS = getSymVal(State, SIE->getLHS());
       RHS = &SIE->getRHS();
     } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
       LHS = &ISE->getLHS();
       RHS = getSymVal(State, ISE->getRHS());
     } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
       // Early termination to avoid expensive call
       LHS = getSymVal(State, SSM->getLHS());
       RHS = LHS ? getSymVal(State, SSM->getRHS()) : nullptr;
     } else {
       llvm_unreachable("Unsupported binary expression to get symbol value!");
     }
 
     if (!LHS || !RHS)
       return nullptr;
 
     llvm::APSInt ConvertedLHS = *LHS, ConvertedRHS = *RHS;
     QualType LTy = getAPSIntType(*LHS), RTy = getAPSIntType(*RHS);
     doIntTypeConversion<llvm::APSInt, Z3ConstraintManager::castAPSInt>(
         ConvertedLHS, LTy, ConvertedRHS, RTy);
-    return BV.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
+    return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS);
   }
 
   llvm_unreachable("Unsupported expression to get symbol value!");
 }
 
 ProgramStateRef
 Z3ConstraintManager::removeDeadBindings(ProgramStateRef State,
                                         SymbolReaper &SymReaper) {

 
 Z3Expr Z3ConstraintManager::getZ3SymBinExpr(const BinarySymExpr *BSE,
                                             bool *hasComparison,
                                             QualType *RetTy) const {
   QualType LTy, RTy;
   BinaryOperator::Opcode Op = BSE->getOpcode();
 
   if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE)) {
-    RTy = getAPSIntType(SIE->getRHS());
+    llvm::APSInt NewRInt;
     Z3Expr LHS = getZ3SymExpr(SIE->getLHS(), &LTy, hasComparison);
-    Z3Expr RHS = Z3Expr::fromAPSInt(SIE->getRHS());
+    Z3Expr RHS = Z3Expr::fromAPSInt(fixAPSInt(SIE->getRHS(), NewRInt, &RTy));
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const IntSymExpr *ISE = dyn_cast<IntSymExpr>(BSE)) {
-    LTy = getAPSIntType(ISE->getLHS());
-    Z3Expr LHS = Z3Expr::fromAPSInt(ISE->getLHS());
+    llvm::APSInt NewLInt;
+    Z3Expr LHS = Z3Expr::fromAPSInt(fixAPSInt(ISE->getLHS(), NewLInt, &LTy));
     Z3Expr RHS = getZ3SymExpr(ISE->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else if (const SymSymExpr *SSM = dyn_cast<SymSymExpr>(BSE)) {
     Z3Expr LHS = getZ3SymExpr(SSM->getLHS(), &LTy, hasComparison);
     Z3Expr RHS = getZ3SymExpr(SSM->getRHS(), &RTy, hasComparison);
     return getZ3BinExpr(LHS, LTy, Op, RHS, RTy, RetTy);
   } else {
     llvm_unreachable("Unsupported BinarySymExpr type!");

 // Helper functions.
 //===------------------------------------------------------------------===//
 
 QualType Z3ConstraintManager::getAPSIntType(const llvm::APSInt &Int) const {
   ASTContext &Ctx = getBasicVals().getContext();
   return Ctx.getIntTypeForBitwidth(Int.getBitWidth(), Int.isSigned());
 }
 
+const llvm::APSInt &Z3ConstraintManager::fixAPSInt(const llvm::APSInt &Int,
+                                                   llvm::APSInt &NewInt,
+                                                   QualType *Ty) const {
+  // 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.
+  if (Int.getBitWidth() == 1 && getAPSIntType(Int).isNull()) {
+    ASTContext &Ctx = getBasicVals().getContext();
+    NewInt = Int.extend(Ctx.getTypeSize(Ctx.BoolTy));
+    if (Ty)
+      *Ty = getAPSIntType(NewInt);
+    return NewInt;
+  }
+
+  if (Ty)
+    *Ty = getAPSIntType(Int);
+  return Int;
+}
+
 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;

 
 #endif
 
 std::unique_ptr<ConstraintManager>
 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
 #if CLANG_ANALYZER_WITH_Z3
   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
 #else
-  llvm::report_fatal_error("Clang was not compiled with Z3 support!", false);
+  llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
+                           "with -DCLANG_ANALYZER_BUILD_Z3=ON",
+                           false);
   return nullptr;
 #endif
 }

test/Analysis/analyzer_test.py

+import copy
 import lit.formats
 import lit.TestRunner
 
 # Custom format class for static analyzer tests
 class AnalyzerTest(lit.formats.ShTest):
 
     def execute(self, test, litConfig):
         results = []
 
         # Parse any test requirements ('REQUIRES: ')
-        saved_test = test
+        saved_test = copy.deepcopy(test)
         lit.TestRunner.parseIntegratedTestScript(test)
 
+        # If the test does not require z3, drop it from the available features
+        # to satisfy tests that explicitly require !z3
         if 'z3' not in test.requires:
+            test.config.available_features.discard('z3')
             results.append(self.executeWithAnalyzeSubstitution(
-                saved_test, litConfig, '-analyzer-constraints=range'))
+                test, litConfig, '-analyzer-constraints=range'))
 
-            if results[-1].code == lit.Test.FAIL:
+            if results[-1].code != lit.Test.PASS:
                 return results[-1]
 
         # If z3 backend available, add an additional run line for it
-        if test.config.clang_staticanalyzer_z3 == '1':
+        if test.config.clang_staticanalyzer_z3 == '1' and '!z3' not in test.requires:
             results.append(self.executeWithAnalyzeSubstitution(
                 saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))
 
         # Combine all result outputs into the last element
         for x in results:
             if x != results[-1]:
                 results[-1].output = x.output + results[-1].output
 

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}}
+    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}}
     return;
   }
   BOOL x = y; // no-warning
 }

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/loop-unrolling.cpp

int nested_inlined_unroll1() {
   }
   int a = 22 / k; // expected-warning {{Division by zero}}
   return 0;
 }
 
 int nested_inlined_no_unroll1() {
   int k;
   for (int i = 0; i < 9; i++) {
+#ifdef ANALYZER_CM_Z3
+    clang_analyzer_numTimesReached(); // expected-warning {{13}}
+#else
     clang_analyzer_numTimesReached(); // expected-warning {{15}}
+#endif
     k = simple_unknown_bound_loop();  // reevaluation without inlining, splits the state as well
   }
   int a = 22 / k; // no-warning
   return 0;
 }
 
 int recursion_unroll1(bool b) {
   int k = 2;

test/Analysis/plist-macros-z3.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
-
+// REQUIRES: z3
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
 
 #define mallocmemory int *x = (int*)malloc(12);
 void noteOnMacro(int y) {
   y++;
   y--;
   mallocmemory
-  y++; 
+  y++;
   y++;
   delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
 }
 
 void macroIsFirstInFunction(int y) {
-  mallocmemory 
+  mallocmemory
   y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
 }
 
 #define checkmacro p==0
 void macroInExpressionAux(bool b);
 int macroInExpression(int *p, int y) {;
   y++;
   macroInExpressionAux(checkmacro);
 
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
 #define noPathNoteMacro y+y
 int macroInExpressionNoNote(int *p, int y) {;
   y++;
   if (5 + noPathNoteMacro)
     if (p)
       ;
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
-#define macroWithArg(mp) mp==0 
+#define macroWithArg(mp) mp==0
 int macroWithArgInExpression(int *p, int y) {;
   y++;
   if (macroWithArg(p))
     ;
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
 #define multiNoteMacroWithError \

 
 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>

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
-
+// REQUIRES: !z3
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
 
 #define mallocmemory int *x = (int*)malloc(12);
 void noteOnMacro(int y) {
   y++;
   y--;
   mallocmemory
-  y++; 
+  y++;
   y++;
   delete x; // expected-warning {{Memory allocated by malloc() should be deallocated by free(), not 'delete'}}
 }
 
 void macroIsFirstInFunction(int y) {
-  mallocmemory 
+  mallocmemory
   y++; // expected-warning {{Potential leak of memory pointed to by 'x'}}
 }
 
 #define checkmacro p==0
 void macroInExpressionAux(bool b);
 int macroInExpression(int *p, int y) {;
   y++;
   macroInExpressionAux(checkmacro);
 
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
 #define noPathNoteMacro y+y
 int macroInExpressionNoNote(int *p, int y) {;
   y++;
   if (5 + noPathNoteMacro)
     if (p)
       ;
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
-#define macroWithArg(mp) mp==0 
+#define macroWithArg(mp) mp==0
 int macroWithArgInExpression(int *p, int y) {;
   y++;
   if (macroWithArg(p))
     ;
   return *p; // expected-warning {{Dereference of null pointer}}
 }
 
 #define multiNoteMacroWithError \

 
 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.
+  if (index - 1 == 0)
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   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.
+  if (index - 1L == 0L)
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f10(long foo)
 {
   unsigned index = -1;
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.
+  if (index - 1UL == 0L)
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
   else
     clang_analyzer_warnIfReached(); // expected-warning{{REACHABLE}}
 }
 
 void f13(int foo)
 {
   unsigned short index = -1;

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) {