[analyzer] Path-sensitive different.IntegerOverflow checker

[j.trofimovich]

Summary

Hi all,

We tried to implement IntegerOverflow checker, which is in the list of potential checkers. Could you review it and share your opinion, please?

Best regards,
Julia Trofimovich

[zaks.anna]

Hi Julia,

Thanks for working on this!

In general, we prefer to get incremental patches rather than something that is close to the end-result. That way it is easier to get the guidance along the way and easier for a reviewer to review.

Here are some high level comments.

The package name lacks description.

It would be very helpful to differentiate the overflows that are considered undefined behavior from the ones that are defined. I would have 2 checkers for these, to allow users to turn them on/off independently. However, this might be a separate future improvement.

Could you add more documentation in doxygen style as well as a high level description of the algorithm?

After briefly looking at the patch, I am still not sure how exactly "ExternalSym" is used. Looks like you are tracking symbols that the analyzer may not have values for (like globals). But that should not be needed: if a value is not known by the analyzer you can determine that when evaluating the overflow check. Specifically, State->assume() returns two states, which you can use to find out which situation you are dealing with:

• there was an overflow
• there was no overflow
• under constrained or unknown - this would correspond to the case where both states are feasible.

There should be other posts on the mailing list describing this API as well as other uses of it throughout the analyzer.

Also, I did not notice tests that are testing these heuristics...

The error message seems to be constructed prematurely and I do not see any tests that test it fully.

Another checker that is somewhat related to this one is the String API checker. One reason why it is still in alpha is that it was very difficult to interpret the reports; most of which were due to overflows earlier on the path. It would be very interesting to see how this checker works on various codebases (with respect to bugs found vs false positives).

Cheers,
Anna.

lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp

35

Are you getting multiple reports on the same location? I don't think that should be happening - the bug reporting infrastructure should unique reports.

349

Need a better comment here - the function returns a bool.
Also, comments should be in doxygen form and added to the declarations.

446

addGoodSink seem to add a symbol to a state. Looks like it's used to track symbols we are not supposed to diagnose - symbols with global state? Could you add a better comment/name here?

Sink has a very specific meaning in the analyzer - it's a node at which the simulation stops. Usually, it's used for unrecoverable error nodes.

498

It looks like you are building an error message string before the issue is diagnosed..

[j.trofimovich]

Thanks a lot for reviewing!

Unfortunately we have no ability to share our code before it satisfies some quality level...

Could you propose description for "different" package?

You are correct in your assumption about ExternalSym goals. But there are some cases where analyzer fails to determine right value for a symbol, i.e two alerts from android codebase:

• report-7f4011.html

File	external/mesa3d/src/glsl/linker.cpp
Location	line 779, column 42
Description	Integer overflow while subtraction. 0 U32b AND 1 U32b

This alert happens because analyzer have no information about num_shaders and while cross_validate_globals proccessing assumes that num_shaders can be 0. But actually it's never happened because num_shaders is checked for 0 every time before link_intrastage_shaders calling (external/mesa3d/src/glsl/linker.cpp, lines 1602 and 1617).

• report-51bc27.html

File	frameworks/av/drm/libdrmframework/plugins/passthru/src/DrmPassthruPlugIn.cpp
Location	line 66, column 41
Description	Integer overflow while addition. 4294967295 U32b AND 1 U32b

This alert happens because constructor for value(line 64) doesn't inlined (because this constructor is defined in another translation unit frameworks/​native/​libs/​utils/​String8.cpp) and class member mString is assumed to be 0. So, when value.length() is called(line 66) underflow happens and (0 - 1) is returned. Further addition 1 results in FP overflow.

We tested IntegerOverflow checker on Android codebase where it produced 236 alerts. In brief I guess about 70% of alerts are TP.

If you would like to inspect full results of analysis with enabled/disabled heuristic please suggest place for uploading(size is about 100mb).

I'll try to change the checker according to your comments and it would be nice if you'll find time to review it again!)

report-7f4011.html221 KBDownload

report-51bc27.html44 KBDownload

[zaks.anna]

Unfortunately we have no ability to share our code before it satisfies some quality level...

The llvm developer policy encourages incremental development. If you cannot send patches before they go though the approval process, maybe you could seek guidance while developing by posting questions on the mailing list and split the patch into logical pieces when sending for review? For example, in this case, the ExternalSym is something that would come in separately with it's own tests as justification. We should also discuss if that's the best approach to suppress the false positives.

You are correct in your assumption about ExternalSym goals. But there are some cases where analyzer fails to determine right value for a symbol, i.e two alerts from android >codebase:

I hope there could be better ways of handling these than a checker keeping a table of symbols that are not handled well by the analyzer. (The current approach does not solve the underlying issues and it introduces overhead for all checkers.)

Looks like there are various sources of false positives..

This alert happens because analyzer have no information about num_shaders and while cross_validate_globals proccessing assumes that num_shaders can be 0. But actually >it's never happened because num_shaders is checked for 0 every time before link_intrastage_shaders calling (external/mesa3d/src/glsl/linker.cpp, lines 1602 and 1617).

This is about an inlined function adding constraints that are not valid for all input values? Would it be possible to construct a small example/test case for this? You can use the debug checkers to show that a particular variable does not have the right value, see docs/analyzer/DebugChecks.rst?

We have added some heuristics for null pointer dereference, where we do not count in the null checks coming from the inlined functions (inlined defensive checks). However, this case might be more complicated.

native/​libs/​utils/​String8.cpp) and class member mString is assumed to be 0. So, when value.length() is called(line 66) underflow happens and (0 - 1) is returned. Further addition 1 results in FP overflow.

It's hard me to tell what this issue is - not all code is available. Again, could you construct a small example and show that the value is wrong with the debug checker? If we fail to inline a constructor, a value should be underconstrained, not '0'.

[j.trofimovich]

Improve checker and test suite:

1. Split into two checkers for def/undef behavior.
2. Refactor message composing
3. Add comments
4. Add test cases

[j.trofimovich]

I'm sorry for two-month delay...
ExternalSym is the only way I can suggest to suppress the large number of FP's. I guess inter-unit analysis could have been helpful, but as such approach would require a lot more work, I found ignoring values which may be changed in other units to be the only viable option. But of course we are interested in any discussions and suggestions...

I've wrote some example but didn't find the proper place to add it, so I guess I just post it here:

main.cpp

#include "SomeClass.h"

void clang_analyzer_eval(bool);

int main() {
  SomeClass sc(0);
  bool b = (sc.someFunc() + 1) != 0;
  // FIXME: 'b' is always TRUE
  clang_analyzer_eval(b); // expected-warning{{TRUE}} expected-warning{{FALSE}}
  return 0;
}

SomeClass.h

#ifndef SOMECLASS_H
#define SOMECLASS_H

void someExternalFunc (int a) {
  unsigned k = a ? 2 * a : a; // A comparison with 0 to bifurcate the state
}

class SomeClass {
  unsigned a;
public:
  SomeClass();
  unsigned someFunc() {
    someExternalFunc(a);
    return a - 1;
  }
};

#endif // SOMECLASS_H

SomeClass.cpp

#include "SomeClass.h"

SomeClass::SomeClass(unsigned pa) {
  a = pa ? pa : -1; // a isn't 0
}

Unexpected "FALSE" warning here has the same nature as the FP in DrmPassthruPlugIn.cpp. Lack of information from another translation unit forces analyzer to consider that some variables may take values which cant't really be taken. So 'b' in main.cpp can't be false, but the 'FALSE' warning still happens.

lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp

35

In what way should bug reporting infrastructure unique reports? scan-build prevents existence of fully identical reports by computing digest (Digest::MD5->new->addfile(*FILE)->hexdigest; scan-build, line 247) but cases when alerts differs by message only aren't caught.

[zaks.anna]

I suspect, this code below explains why you are getting the false positives.

The issue you highlight in the example is that sometimes the analyzer doesn't know what the value of a variable is. The existing checkers minimize false positives by issuing a warning only when it's known that a value is "bad". For example, we would only warn if StateOverflow && !StateNotOverflow. This will flag much less issues, but should not produce a lot of false positives.

Are the false positives you are getting being flagged by the first if clause?

if (StateOverflow && StateNotOverflow) {

  if (Pack.LValueIsTainted) {
    Msg.assign("Possible integer overflow while " + Pack.Operation +
               ". Left operand is tainted: " + Pack.LValue + " AND " +
               Pack.RValue);
    reportBug(Msg, C, SL);
  } else if (Pack.RValueIsTainted) {
    Msg.assign("Possible integer overflow while " + Pack.Operation +
               ". Right operand is tainted: " + Pack.LValue + " AND " +
               Pack.RValue);
    reportBug(Msg, C, SL);
  }
  return;
}

if (StateOverflow) {
  Msg.assign("Integer overflow while " + Pack.Operation + ". " + Pack.LValue +
             " AND " + Pack.RValue);
  reportBug(Msg, C, SL);
}

lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp

35

Identical issues should have the same message. Do you have identical issues with different messages?

[j.trofimovich]

Hello Anna,

thank you for your reply.
Could you please point a problem in this code sample? I cannot find a sample that doesn't follow this recommendation.
In this checker, we have 2 cases for throwing a report:

1. We could both overflow and not overflow (StateOverflow && StateNotOverflow). So I check if one of operands is tainted, produce a warning if so and return. It is not a source of false positives.
2. Then I check if only overflow is possible: StateOverflow && !StateNotOverflow == StateOverflow here, because StateOverflow && StateNotOverflow option was considered before.

I'll try to explain my assumptions why having 'StateOverflow && !StateNotOverflow' is not enough to get a reliable reason to warn.
The first 'if' clause is not a problem because we could definitely know if an operand is tainted so we point that we *can* overflow here. The main source of false positives are values that are reasoned to overflow by analyzer but cannot overflow due to possible checks in the caller. These values are values of function arguments and global variables, for example. I collect these values in 'ExternalSym' set. This is what I am filtering out. In this case analyzer's constraints are not enough to suggest an overflow so we make an additional check.

lib/StaticAnalyzer/Checkers/Checkers.td

 def DeadCode : Package<"deadcode">;
 def DeadCodeAlpha : Package<"deadcode">, InPackage<Alpha>, Hidden;
 
+def Different : Package<"different">;
+def DifferentAlpha : Package<"different">, InPackage<Alpha>, Hidden;
+
 def Security : Package <"security">;
 def InsecureAPI : Package<"insecureAPI">, InPackage<Security>;
 def SecurityAlpha : Package<"security">, InPackage<Alpha>, Hidden;
 def Taint : Package<"taint">, InPackage<SecurityAlpha>, Hidden;  
 
+def UndefBehavior : Package<"undefbehavior">;
+def UndefBehaviorAlpha : Package<"undefbehavior">, InPackage<Alpha>, Hidden;
+
 def Unix : Package<"unix">;
 def UnixAlpha : Package<"unix">, InPackage<Alpha>, Hidden;
 def CString : Package<"cstring">, InPackage<Unix>, Hidden;

 def CoreFoundation : Package<"coreFoundation">, InPackage<OSX>;
 def Containers : Package<"containers">, InPackage<CoreFoundation>;
 
-def Different : Package<"different">;
-def DifferentAlpha : Package<"different">, InPackage<Alpha>, Hidden;
-
 def LLVM : Package<"llvm">;
 def Debug : Package<"debug">;
 

 } // end "alpha.deadcode"
 
 //===----------------------------------------------------------------------===//
+// Different checkers.
+//===----------------------------------------------------------------------===//
+
+let ParentPackage = DifferentAlpha in {
+
+def IntegerOverflowDef : Checker<"IntegerOverflow">,
+  HelpText<"Check for integer overflow resulting in defined behavior only">,
+  DescFile<"IntegerOverflowChecker.cpp">;
+
+} // end "alpha.different"
+
+//===----------------------------------------------------------------------===//
 // Security checkers.
 //===----------------------------------------------------------------------===//
 

 } // end "alpha.security.taint"
 
 //===----------------------------------------------------------------------===//
+// Undefined behavior checkers.
+//===----------------------------------------------------------------------===//
+
+let ParentPackage = UndefBehaviorAlpha in {
+
+def IntegerOverflowUndef : Checker<"IntegerOverflow">,
+  HelpText<"Check for integer overflow resulting in undefined behavior">,
+  DescFile<"IntegerOverflowChecker.cpp">;
+
+} // end "alpha.undefbehavior"
+
+//===----------------------------------------------------------------------===//
 // Unix API checkers.
 //===----------------------------------------------------------------------===//
 

 }
 
 //===----------------------------------------------------------------------===//
-// Different checkers.
-//===----------------------------------------------------------------------===//
-
-def IntegerOverflowChecker : Checker<"IntegerOverflow">,
-  InPackage<DifferentAlpha>,
-  HelpText<"Check for integer overflow">,
-  DescFile<"IntegerOverflowChecker.cpp">;
-
-
-//===----------------------------------------------------------------------===//
 // Checkers for LLVM development.
 //===----------------------------------------------------------------------===//
 

lib/StaticAnalyzer/Checkers/IntegerOverflowChecker.cpp

 // License. See LICENSE.TXT for details.
 //
 //===----------------------------------------------------------------------===//
+///
+/// \file
+/// \brief This defines IntegerOverflowChecker, which checks arithmetic
+/// operations for integer overflows. This check corresponds to CWE-190.
+///
+//===----------------------------------------------------------------------===//
+//
+// Check for overflow performs by checkAdd(), checkSub() and checkMul()
+// functions. checkAdd() and checkSub() consist of two parts for signed integer
+// overflow check and unsigned integer overflow check(wraparound).
 //
-// This file defines IntegerOverflowChecker, which checks arithmetic operations
-// for integer overflows. This check corresponds to CWE-190.
+// Couple of heuristics were added for FP suppressing. USubHeuristic prevents
+// warnings for intentional integer overflow while getting i.e UINT_MAX by
+// subtracting 1U from 0U. GlobalsMembersHeuristic suppresses warning if
+// arguments of arithmetic operation are global variables or class members.
+// Sometimes CSA fails to determine right value for that type of arguments and
+// inter-unit analysis assumed to be the best solution of this problem.
 //
 //===----------------------------------------------------------------------===//
 

                                               check::PostStmt<CallExpr>,
                                               check::PostStmt<MemberExpr>,
                                               check::Bind> {
-  mutable std::unique_ptr<BuiltinBug> BT;
+  mutable std::unique_ptr<BuiltinBug> BT_Def, BT_Undef;
 
+  /// Stores SourceLocations in which overflows happened for reducing the amount
+  /// of equivalent warnings.
   mutable std::set<SourceLocation> OverflowLoc;
 
-  struct OutputPack {
-    const bool LValueIsTainted;
-    const bool RValueIsTainted;
-    const std::string LValue;
-    const std::string RValue;
-    std::string Operation;
-    OutputPack(bool LValueIsTainted, bool RValueIsTainted,
-               const std::string &LValue, const std::string &RValue)
-        : LValueIsTainted(LValueIsTainted), RValueIsTainted(RValueIsTainted),
-          LValue(LValue), RValue(RValue) {}
+  struct IntegerOverflowFilter {
+    DefaultBool CheckIntegerOverflowDef;
+    DefaultBool CheckIntegerOverflowUndef;
+    CheckName CheckNameIntegerOverflowDef;
+    CheckName CheckNameIntegerOverflowUndef;
   };
 
   void reportBug(const std::string &Msg, CheckerContext &C,
-                 const SourceLocation &SL) const;
+                 const SourceLocation &SL, bool isUndef) const;
+
+  std::string composeMsg(ProgramStateRef StateNotOverflow, const SVal &Lhs,
+                         const SVal &Rhs, const Expr *ExprLhs,
+                         const Expr *ExprRhs, bool isSigned, bool isOverflow,
+                         BinaryOperator::Opcode *Op, CheckerContext &C) const;
 
+  /// Check if addition of \p Lhs and \p Rhs can overflow.
   Optional<DefinedOrUnknownSVal> checkAdd(CheckerContext &C, const SVal &Lhs,
-                                          const SVal &Rhs,
-                                          QualType BinType) const;
+                                          const SVal &Rhs, QualType BinType,
+                                          bool &isOverflow) const;
 
+  /// Check if subtraction of \p Lhs and \p Rhs can overflow.
   Optional<DefinedOrUnknownSVal> checkSub(CheckerContext &C, const SVal &Lhs,
                                           const SVal &Rhs,
-                                          const QualType &BinType) const;
+                                          const QualType &BinType,
+                                          bool &isOverflow) const;
 
+  /// Check if multiplication of \p Lhs and \p Rhs can overflow.
   Optional<DefinedOrUnknownSVal> checkMul(CheckerContext &C, const SVal &Lhs,
                                           const SVal &Rhs,
-                                          const QualType &BinType) const;
-
-  void addRangeInformation(const SVal &Val, CheckerContext &C,
-                           llvm::raw_string_ostream &Stream) const;
+                                          const QualType &BinType,
+                                          bool &isOverflow) const;
 
-  void processStates(ProgramStateRef StateOverflow,
-                     ProgramStateRef StateNotOverflow, const OutputPack &Pack,
-                     CheckerContext &C, const SourceLocation &SL) const;
+  /// \returns dump and constraints of \p Val.
+  std::string getSymbolInformation(const SVal &Val, const Expr *E,
+                                   CheckerContext &C) const;
 
+  /// We ignore intentional underflow because of subtracting X from zero - the
+  /// minimum unsigned value.
   bool makeUSubHeuristics(const BinaryOperator *BO) const;
 
+  /// \returns true if there are suspicions that the actual value might be lose
+  /// by analyzer.
   bool makeGlobalsMembersHeuristics(const SVal &Val, const Stmt *S,
                                     CheckerContext &C) const;
 
+  /// Check if \p S should be ignored when participates in overflow.
   bool hasGlobalVariablesOrMembers(const Stmt *S, CheckerContext &C) const;
 
+  /// Check if \p SE should be ignored when participates in overflow.
   bool hasGlobalVariablesOrMembers(const SymExpr *SE, CheckerContext &C) const;
 
-  ProgramStateRef addGoodSink(const Stmt *S, ProgramStateRef State,
+  ProgramStateRef addToWhiteList(const Stmt *S, ProgramStateRef State,
                                  const LocationContext *LCtx) const;
 
-  inline ProgramStateRef addGoodSink(const SVal &SV,
+  inline ProgramStateRef addToWhiteList(const SVal &SV,
                                         ProgramStateRef State) const;
 
-  bool isGoodSink(const Stmt *S, ProgramStateRef State,
+  bool isInWhiteList(const Stmt *S, ProgramStateRef State,
                      const LocationContext *LCtx) const;
 
-  inline bool isGoodSink(const SVal &Val, ProgramStateRef State) const;
+  inline bool isInWhiteList(const SVal &Val, ProgramStateRef State) const;
 
 public:
-  /// \brief Contains checks for such operations as addition, multiplication,
-  /// and subtraction.
-  void checkPreStmt(const BinaryOperator *B, CheckerContext &C) const;
+  IntegerOverflowFilter Filter;
 
-  /// \brief Contains check for new[].
+  /// Check addition, multiplication, and subtraction for overflow.
+  void checkPostStmt(const BinaryOperator *B, CheckerContext &C) const;
+
+  /// Contains check for new[].
   void checkPostStmt(const CXXNewExpr *NE, CheckerContext &C) const;
 
+  /// Note if value returned by a call should be ignored when participates in
+  /// overflow.
   void checkPostStmt(const CallExpr *CE, CheckerContext &C) const;
 
+  /// Make MemberExpr ignored.
   void checkPostStmt(const MemberExpr *ME, CheckerContext &C) const;
 
+  /// Note if value which is handled by checkBind should be ignored when
+  /// participates in overflow.
   void checkBind(const SVal &Loc, const SVal &Val, const Stmt *S,
                  CheckerContext &C) const;
 };
 } // end anonymous namespace
 
-REGISTER_LIST_WITH_PROGRAMSTATE(ExternalSym, SVal)
+/// WhiteList stores symbols change of which can be missed by analyzer.
+REGISTER_LIST_WITH_PROGRAMSTATE(WhiteList, SVal)
 
 void IntegerOverflowChecker::reportBug(const std::string &Msg,
                                        CheckerContext &C,
-                                       const SourceLocation &SL) const {
+                                       const SourceLocation &SL,
+                                       bool isUndef) const {
   if (const ExplodedNode *N = C.generateSink(C.getState())) {
-    if (!BT)
-      BT.reset(new BuiltinBug("Integer overflow"));
-
-    BugReport *R = new BugReport(*BT, Msg, N);
+    if (isUndef && !BT_Undef)
+      BT_Undef.reset(new BuiltinBug(
+          Filter.CheckNameIntegerOverflowUndef, "Integer overflow",
+          "Arithmetic operation resulted in an overflow"));
+    else if (!isUndef && !BT_Def)
+      BT_Def.reset(
+          new BuiltinBug(Filter.CheckNameIntegerOverflowDef, "Integer overflow",
+                         "Arithmetic operation resulted in an overflow"));
+    BugReport *R = new BugReport(isUndef ? *BT_Undef : *BT_Def, Msg, N);
     C.emitReport(R);
     OverflowLoc.insert(SL);
   }
 }
 
+std::string
+IntegerOverflowChecker::composeMsg(ProgramStateRef StateNotOverflow,
+                                   const SVal &Lhs, const SVal &Rhs,
+                                   const Expr *ExprLhs, const Expr *ExprRhs,
+                                   bool isSigned, bool isOverflow,
+                                   BinaryOperator::Opcode *Op,
+                                   CheckerContext &C) const {
+  std::string Msg;
+  std::string ErrorType = (!Op || isOverflow) ? "Overflow" : "Underflow";
+  if (StateNotOverflow) {
+    Msg.assign("Possible integer " + ErrorType + ": ");
+    if (C.getState()->isTainted(Lhs))
+      Msg.append("left operand is tainted. ");
+    else
+      Msg.append("right operand is tainted. ");
+  } else {
+    if (isSigned)
+      Msg.assign("Undefined behavior: ");
+
+    Msg.append("Integer " + ErrorType + ". ");
+  }
+  std::string Operation, Preposition;
+
+  if (!Op || *Op == BO_Mul || *Op == BO_MulAssign) {
+    Operation = "Multiplication of ";
+    Preposition = " with ";
+  } else if (*Op == BO_Add || *Op == BO_AddAssign) {
+    Operation = "Addition of ";
+    Preposition = " with ";
+  } else {
+    Operation = "Subtraction of ";
+    Preposition = " from ";
+  }
+
+  if (Op && (*Op == BO_Sub || (*Op == BO_SubAssign)))
+    Msg.append(Operation + getSymbolInformation(Rhs, ExprRhs, C) + Preposition +
+               getSymbolInformation(Lhs, ExprLhs, C));
+  else
+    Msg.append(Operation + getSymbolInformation(Lhs, ExprLhs, C) + Preposition +
+               getSymbolInformation(Rhs, ExprRhs, C));
+
+  if (!Op)
+    Msg.append(" while memory allocation.");
+
+  return Msg;
+}
+
 Optional<DefinedOrUnknownSVal>
 IntegerOverflowChecker::checkAdd(CheckerContext &C, const SVal &Lhs,
-                                 const SVal &Rhs, QualType BinType) const {
+                                 const SVal &Rhs, QualType BinType,
+                                 bool &isOverflow) const {
   SVal CondOverflow;
   ProgramStateRef State = C.getState();
   SValBuilder &SvalBuilder = C.getSValBuilder();

     SVal CondNegativeOverflow =
         SvalBuilder.evalBinOp(State, BO_And, CondArgsLtNull, CondArgSumGtNull,
                               CondType);
+    if (!CondPositiveOverflow.isZeroConstant())
+      isOverflow = true;
 
     CondOverflow = SvalBuilder.evalBinOp(State, BO_Or, CondPositiveOverflow,
                                          CondNegativeOverflow, CondType);
   } else {
+    isOverflow = true;
     // lhs > sum
     SVal CondLhsGtArgSum = SvalBuilder.evalBinOp(State, BO_GT, Lhs, ValArgSum,
                                                  CondType);

 
 Optional<DefinedOrUnknownSVal>
 IntegerOverflowChecker::checkSub(CheckerContext &C, const SVal &Lhs,
-                                 const SVal &Rhs,
-                                 const QualType &BinType) const {
+                                 const SVal &Rhs, const QualType &BinType,
+                                 bool &isOverflow) const {
   SVal CondOverflow;
   ProgramStateRef State = C.getState();
   SValBuilder &SvalBuilder = C.getSValBuilder();

     SVal CondLhsLtNullRhsGtNull =
         SvalBuilder.evalBinOp(State, BO_And, CondLhsLtNull, CondRhsGtNull,
                               CondType);
-    // lhs-rhs >= 0
+    // lhs - rhs >= 0
     SVal CondArgSubGeNull = SvalBuilder.evalBinOp(State, BO_GE, ValArgSub,
                                                   NullSval, CondType);
 

 
     CondOverflow = SvalBuilder.evalBinOp(State, BO_Or, CondNegativeOverflow,
                                          CondPositiveOverflow, CondType);
+    if (!CondPositiveOverflow.isZeroConstant())
+      isOverflow = true;
   } else
     CondOverflow = SvalBuilder.evalBinOp(State, BO_LT, Lhs, Rhs, CondType);
 

 
 Optional<DefinedOrUnknownSVal>
 IntegerOverflowChecker::checkMul(CheckerContext &C, const SVal &Lhs,
-                                 const SVal &Rhs,
-                                 const QualType &BinType) const {
+                                 const SVal &Rhs, const QualType &BinType,
+                                 bool &isOverflow) const {
   ProgramStateRef State = C.getState();
   ProgramStateRef CondNotOverflow, CondPossibleOverflow;
   SValBuilder &SvalBuilder = C.getSValBuilder();

   if (!CondOverflow.hasValue())
     return CondOverflow;
 
-  llvm::tie(CondPossibleOverflow, CondNotOverflow) =
+  std::tie(CondPossibleOverflow, CondNotOverflow) =
       State->assume(*CondOverflow);
 
   if (CondNotOverflow && CondPossibleOverflow)

     CondOverflow = SvalBuilder.evalBinOp(State, BO_NE, ValDiv, Rhs, CondType)
                        .getAs<DefinedOrUnknownSVal>();
   }
+
+  isOverflow = BinType->isUnsignedIntegerOrEnumerationType() ||
+               SvalBuilder.evalBinOp(State, BO_LT, Lhs, NullSval, CondType)
+                       .isZeroConstant() ==
+                   SvalBuilder.evalBinOp(State, BO_LT, Rhs, NullSval, CondType)
+                       .isZeroConstant();
+
   return CondOverflow;
 }
 
-void IntegerOverflowChecker::addRangeInformation(
-    const SVal &Val, CheckerContext &C,
-    llvm::raw_string_ostream &Stream) const {
-  std::string S;
-  llvm::raw_string_ostream StreamRange(S);
-  if (Val.getSubKind() == nonloc::SymbolValKind) {
-    C.getState()->getConstraintManager().print(C.getState(), StreamRange, "\n",
-                                               "\n");
-    size_t from = StreamRange.str().find(Stream.str() + " : ");
+std::string
+IntegerOverflowChecker::getSymbolInformation(const SVal &Val, const Expr *E,
+                                             CheckerContext &C) const {
+  ProgramStateRef State = C.getState();
+  std::string StreamRangeStr, SValDumpStr;
+  llvm::raw_string_ostream StreamRange(StreamRangeStr), SValDump(SValDumpStr);
+  Val.dumpToStream(SValDump);
+  if (Val.getSubKind() == SymbolValKind) {
+    State->getConstraintManager().print(State, StreamRange, "\n", "\n");
+    StreamRange.flush();
+    size_t from = StreamRangeStr.find(SValDump.str() + " : ");
     if (from != std::string::npos) {
-      size_t to = StreamRange.str().find("\n", from);
-      from += Stream.str().length();
-      Stream << StreamRange.str().substr(from, to - from);
+      size_t to = StreamRangeStr.find("\n", from);
+      from += SValDump.str().length();
+      SValDump.str().append(StreamRangeStr.substr(from, to - from));
     }
   }
-}
+  if (!E || isa<IntegerLiteral>(E->IgnoreParenCasts()))
+    return SValDump.str();
 
-void IntegerOverflowChecker::processStates(ProgramStateRef StateOverflow,
-                                           ProgramStateRef StateNotOverflow,
-                                           const OutputPack &Pack,
-                                           CheckerContext &C,
-                                           const SourceLocation &SL) const {
-  std::string Msg;
-  if (StateOverflow && StateNotOverflow) {
-    if (Pack.LValueIsTainted) {
-      Msg.assign("Possible integer overflow while " + Pack.Operation +
-                 ". Left operand is tainted: " + Pack.LValue + " AND " +
-                 Pack.RValue);
-      reportBug(Msg, C, SL);
-    } else if (Pack.RValueIsTainted) {
-      Msg.assign("Possible integer overflow while " + Pack.Operation +
-                 ". Right operand is tainted: " + Pack.LValue + " AND " +
-                 Pack.RValue);
-      reportBug(Msg, C, SL);
-    }
-    return;
-  }
+  E = E->IgnoreParens();
+  if (const UnaryOperator *UO = dyn_cast<UnaryOperator>(E))
+    if ((UO->getOpcode() == UO_Plus || UO->getOpcode() == UO_Minus) &&
+        isa<IntegerLiteral>(UO->getSubExpr()))
+      return SValDump.str();
 
-  if (StateOverflow) {
-    Msg.assign("Integer overflow while " + Pack.Operation + ". " + Pack.LValue +
-               " AND " + Pack.RValue);
-    reportBug(Msg, C, SL);
-  }
+  SValDump << " (";
+  E->printPretty(SValDump, 0, C.getASTContext().getPrintingPolicy());
+  SValDump << ")";
+
+  return SValDump.str();
 }
 
 // We ignore intentional underflow with subtracting X from zero - the minimal

   return false;
 }
 
-// Don't track global variables and class members we can't reason about.
 bool
 IntegerOverflowChecker::makeGlobalsMembersHeuristics(const SVal &Val,
                                                      const Stmt *S,
                                                      CheckerContext &C)const {
   if (Val.isConstant()) {
-    bool good = isGoodSink(Val, C.getState()) &&
+    bool good = isInWhiteList(Val, C.getState()) &&
                 (S->getStmtClass() != Stmt::IntegerLiteralClass) &&
                 (S->getStmtClass() != Stmt::ImplicitCastExprClass);
     return good ? true : hasGlobalVariablesOrMembers(S, C);
   } else if (const SymExpr *SE = Val.getAsSymExpr())
-    return isGoodSink(Val, C.getState()) ? true
+    return isInWhiteList(Val, C.getState()) ? true
                                             : hasGlobalVariablesOrMembers(SE, C);
   else if (const MemRegion *Mem = Val.getAsRegion())
-    return isGoodSink(Val, C.getState()) || isa<FieldRegion>(Mem) ||
+    return isInWhiteList(Val, C.getState()) || isa<FieldRegion>(Mem) ||
            Mem->hasGlobalsOrParametersStorage();
 
   return false;

   const LocationContext *LCtx = C.getLocationContext();
 
   if ((S->getStmtClass() != Stmt::ImplicitCastExprClass) &&
-      isGoodSink(S, State, LCtx))
+      isInWhiteList(S, State, LCtx))
     return true;
 
   if (const MemberExpr *MExpr = dyn_cast<MemberExpr>(S)) {

   }
 
   if (const ImplicitCastExpr *ICE = dyn_cast<ImplicitCastExpr>(S))
-    if (isa<DeclRefExpr>(ICE->getSubExpr()) && isGoodSink(C.getSVal(ICE),
+    if (isa<DeclRefExpr>(ICE->getSubExpr()) && isInWhiteList(C.getSVal(ICE),
                                                              State))
         return true;
 
   if (const DeclRefExpr *DRE = dyn_cast<DeclRefExpr>(S))
     if (const VarDecl *VarD = dyn_cast<VarDecl>(DRE->getDecl())) {
       Loc VLoc = C.getStoreManager().getLValueVar(VarD, LCtx);
       SVal VVal = C.getStoreManager().getBinding(State->getStore(), VLoc);
-      if (isGoodSink(VVal, State))
+      if (isInWhiteList(VVal, State))
         return true;
     }
 
   // We will not surrender!
-  for (clang::Stmt::const_child_iterator I = S->child_begin();
-       I != S->child_end(); I++)
+  for (auto I = S->child_begin(); I != S->child_end(); I++)
     if (hasGlobalVariablesOrMembers(*I, C))
       return true;
 

 bool
 IntegerOverflowChecker::hasGlobalVariablesOrMembers(const SymExpr *SE,
                                                     CheckerContext &C) const {
-  ExternalSymTy ES = C.getState()->get<ExternalSym>();
-  for (ExternalSymTy::iterator I = ES.begin(); I != ES.end(); ++I) {
+  WhiteListTy ES = C.getState()->get<WhiteList>();
+  for (auto I = ES.begin(); I != ES.end(); ++I) {
     SVal Val = *I;
     SymbolRef SR = Val.getAsSymbol();
     if (SR == SE)

 }
 
 ProgramStateRef
-IntegerOverflowChecker::addGoodSink(const Stmt *S, ProgramStateRef State,
+IntegerOverflowChecker::addToWhiteList(const Stmt *S, ProgramStateRef State,
                                        const LocationContext *LCtx) const {
   if (const Expr *E = dyn_cast_or_null<Expr>(S))
     S = E->IgnoreParens();
-  return addGoodSink(State->getSVal(S, LCtx), State);
+  return addToWhiteList(State->getSVal(S, LCtx), State);
 }
 
 inline ProgramStateRef
-IntegerOverflowChecker::addGoodSink(const SVal &Val,
+IntegerOverflowChecker::addToWhiteList(const SVal &Val,
                                        ProgramStateRef State) const {
-  return State->get<ExternalSym>().contains(Val) ? State
-                                                 : State->add<ExternalSym>(Val);
+  return State->get<WhiteList>().contains(Val) ? State
+                                               : State->add<WhiteList>(Val);
 }
 
-// Returns true, if given Stmt contains global variables/class members.
-bool IntegerOverflowChecker::isGoodSink(const Stmt *S, ProgramStateRef State,
-                                        const LocationContext *LCtx) const {
+bool IntegerOverflowChecker::isInWhiteList(const Stmt *S, ProgramStateRef State,
+                                           const LocationContext *LCtx) const {
   if (const Expr *E = dyn_cast_or_null<Expr>(S))
     S = E->IgnoreParens();
-  return isGoodSink(State->getSVal(S, LCtx), State);
+  return isInWhiteList(State->getSVal(S, LCtx), State);
 }
 
-inline bool IntegerOverflowChecker::isGoodSink(const SVal &V,
+inline bool IntegerOverflowChecker::isInWhiteList(const SVal &V,
                                                   ProgramStateRef State) const {
-  return State->get<ExternalSym>().contains(V);
+  return State->get<WhiteList>().contains(V);
 }
 
 void IntegerOverflowChecker::checkPostStmt(const BinaryOperator *B,

       !B->getRHS()->getType()->isIntegerType())
     return;
 
-  BinaryOperator::Opcode Op = B->getOpcode();
-  if (Op!=BO_Add && Op!=BO_Mul && Op!=BO_Sub)
-    return;
-
   ProgramStateRef State = C.getState();
   QualType BinType = B->getType();
   const Expr *ExprLhs = B->getLHS();

   SVal Lhs = C.getSVal(ExprLhs);
   SVal Rhs = C.getSVal(ExprRhs);
 
-  //if (makeConjHeuristics(Lhs) || makeConjHeuristics(Rhs)) return;
-
-  SVal CondOverflow;
-  ProgramStateRef StateOverflow, StateNotOverflow;
-
-  std::string SLvalue, SRvalue;
-  llvm::raw_string_ostream LValue(SLvalue), RValue(SRvalue);
-  Lhs.dumpToStream(LValue);
-  Rhs.dumpToStream(RValue);
-
-  addRangeInformation(Rhs, C, RValue);
-  addRangeInformation(Lhs, C, LValue);
-
   if (makeGlobalsMembersHeuristics(Lhs, ExprLhs, C)) {
-    C.addTransition(addGoodSink(Lhs, State));
+    C.addTransition(addToWhiteList(Lhs, State));
     return;
   }
   if (makeGlobalsMembersHeuristics(Rhs, ExprRhs, C)) {
-    C.addTransition(addGoodSink(Rhs, State));
+    C.addTransition(addToWhiteList(Rhs, State));
     return;
   }
 
+  if (!Filter.CheckIntegerOverflowDef && BinType->isUnsignedIntegerType())
+    return;
+
+  if (!Filter.CheckIntegerOverflowUndef && BinType->isSignedIntegerType())
+    return;
+
   BinaryOperator::Opcode Op = B->getOpcode();
   if (Op != BO_Add && Op != BO_Mul && Op != BO_Sub && Op != BO_AddAssign &&
       Op != BO_MulAssign && Op != BO_SubAssign)

   Optional<DefinedOrUnknownSVal> CondOverflow;
   ProgramStateRef StateOverflow, StateNotOverflow;
 
-  OutputPack Pack(State->isTainted(Lhs), State->isTainted(Rhs), LValue.str(),
-                  RValue.str());
-
-  if (Op == BO_Add || Op == BO_AddAssign) {
-    CondOverflow = checkAdd(C, Lhs, Rhs, BinType);
-    if (!CondOverflow)
-      return;
-
-    llvm::tie(StateOverflow, StateNotOverflow) = State->assume(*CondOverflow);
-
-    Pack.Operation = "addition";
-
-    processStates(StateOverflow, StateNotOverflow, Pack, C, B->getExprLoc());
-  } else if (Op == BO_Sub || Op == BO_SubAssign) {
+  bool isOverflow = false;
+  if (Op == BO_Add || Op == BO_AddAssign)
+    CondOverflow = checkAdd(C, Lhs, Rhs, BinType, isOverflow);
+  else if (Op == BO_Sub || Op == BO_SubAssign) {
     if ((BinType->isUnsignedIntegerType()) && makeUSubHeuristics(B))
       return;
+    CondOverflow = checkSub(C, Lhs, Rhs, BinType, isOverflow);
+  } else if (Op == BO_Mul || Op == BO_MulAssign)
+    CondOverflow = checkMul(C, Lhs, Rhs, BinType, isOverflow);
 
-    CondOverflow = checkSub(C, Lhs, Rhs, BinType);
-    if (!CondOverflow)
-      return;
-
-    llvm::tie(StateOverflow, StateNotOverflow) = State->assume(*CondOverflow);
-
-    Pack.Operation = "subtraction";
-
-    processStates(StateOverflow, StateNotOverflow, Pack, C, B->getExprLoc());
-  } else if (Op == BO_Mul || Op == BO_MulAssign) {
-    CondOverflow = checkMul(C, Lhs, Rhs, BinType);
+  if (!CondOverflow)
+    return;
 
-    if (!CondOverflow)
-      return;
+  std::tie(StateOverflow, StateNotOverflow) = State->assume(*CondOverflow);
 
-    llvm::tie(StateOverflow, StateNotOverflow) = State->assume(*CondOverflow);
+  if (!StateOverflow ||
+      (StateNotOverflow && !(State->isTainted(Lhs) || State->isTainted(Rhs))))
+    return;
 
-    Pack.Operation = "multiplication";
+  std::string Msg = composeMsg(StateNotOverflow, Lhs, Rhs, ExprLhs, ExprRhs,
+                               B->getType()->isSignedIntegerOrEnumerationType(),
+                               isOverflow, &Op, C);
 
-    processStates(StateOverflow, StateNotOverflow, Pack, C, B->getExprLoc());
-  }
+  reportBug(Msg, C, B->getExprLoc(), BinType->isSignedIntegerType());
 }
 
 void IntegerOverflowChecker::checkPostStmt(const CXXNewExpr *NewExpr,
                                            CheckerContext &C) const {
-  if (NewExpr->getOperatorNew()->getOverloadedOperator() != OO_Array_New)
+  if (!Filter.CheckIntegerOverflowDef)
     return;
 
-  SValBuilder &SvalBuilder = C.getSValBuilder();
-  QualType NewExprType = NewExpr->getAllocatedType();
-
-  uint64_t NewExprTypeSize = C.getASTContext().getTypeSizeInChars(NewExprType)
-                                              .getQuantity();
-  SVal NewExprTypeSizeVal = SvalBuilder.makeIntVal(NewExprTypeSize, true);
+  if (NewExpr->getOperatorNew()->getOverloadedOperator() != OO_Array_New)
+    return;
 
   const Expr *ArrSize = NewExpr->getArraySize();
   SVal ElementCount = C.getSVal(ArrSize);
   ProgramStateRef State = C.getState();
-  ProgramStateRef StateOverflow, StateNotOverflow;
 
   if (makeGlobalsMembersHeuristics(ElementCount, ArrSize, C)) {
-    C.addTransition(addGoodSink(ElementCount, State));
+    C.addTransition(addToWhiteList(ElementCount, State));
     return;
   }
 
-  std::string SLvalue, SRvalue;
-  llvm::raw_string_ostream LValue(SLvalue), RValue(SRvalue);
-  LValue << NewExprTypeSize;
-  ElementCount.dumpToStream(RValue);
-
-  addRangeInformation(ElementCount, C, RValue);
-
-  OutputPack Pack(false, State->isTainted(ElementCount), LValue.str(),
-                  RValue.str());
+  QualType NewExprType = NewExpr->getAllocatedType();
+  uint64_t NewExprTypeSize = C.getASTContext().getTypeSizeInChars(NewExprType)
+                                              .getQuantity();
+  SValBuilder &SvalBuilder = C.getSValBuilder();
+  SVal NewExprTypeSizeVal = SvalBuilder.makeIntVal(NewExprTypeSize, true);
 
-  Optional<DefinedOrUnknownSVal> CondOverflow =
-      checkMul(C, NewExprTypeSizeVal, ElementCount, ArrSize->getType());
+  bool isOverflow;
+  Optional<DefinedOrUnknownSVal> CondOverflow = checkMul(C, NewExprTypeSizeVal,
+                                                         ElementCount,
+                                                         ArrSize->getType(),
+                                                         isOverflow);
 
   if (!CondOverflow)
     return;
 
+  ProgramStateRef StateOverflow, StateNotOverflow;
   std::tie(StateOverflow, StateNotOverflow) = State->assume(*CondOverflow);
 
-  Pack.Operation = "memory allocation";
+  if (!StateOverflow || (StateNotOverflow && !State->isTainted(ElementCount)))
+    return;
+
+  std::string Msg = composeMsg(StateNotOverflow, NewExprTypeSizeVal,
+                               ElementCount, 0, ArrSize, false, isOverflow, 0,
+                               C);
 
-  processStates(StateOverflow, StateNotOverflow, Pack, C,
-                NewExpr->getExprLoc());
+  reportBug(Msg, C, NewExpr->getExprLoc(), false);
 }
 
 void IntegerOverflowChecker::checkPostStmt(const CallExpr *CE,
                                            CheckerContext &C) const {
   if (makeGlobalsMembersHeuristics(C.getSVal(CE), CE, C))
-    C.addTransition(addGoodSink(CE, C.getState(), C.getLocationContext()));
+    C.addTransition(addToWhiteList(CE, C.getState(), C.getLocationContext()));
 }
 
 void IntegerOverflowChecker::checkPostStmt(const MemberExpr *ME,
                                            CheckerContext &C) const {
-  C.addTransition(addGoodSink(ME, C.getState(), C.getLocationContext()));
+  C.addTransition(addToWhiteList(ME, C.getState(), C.getLocationContext()));
 }
 
 void IntegerOverflowChecker::checkBind(const SVal &Loc, const SVal &Val,
                                        const Stmt *S, CheckerContext &C) const {
   if (makeGlobalsMembersHeuristics(Val, S, C))
-    C.addTransition(addGoodSink(Val, C.getState()));
+    C.addTransition(addToWhiteList(Val, C.getState()));
 }
 
-void ento::registerIntegerOverflowChecker(CheckerManager &mgr) {
-  mgr.registerChecker<IntegerOverflowChecker>();
-}
+#define REGISTER_CHECKER(name)                                                 \
+  void ento::register##name(CheckerManager &mgr) {                             \
+    IntegerOverflowChecker *checker =                                          \
+        mgr.registerChecker<IntegerOverflowChecker>();                         \
+    checker->Filter.Check##name = true;                                        \
+    checker->Filter.CheckName##name = mgr.getCurrentCheckName();               \
+  }
+
+REGISTER_CHECKER(IntegerOverflowDef)
+REGISTER_CHECKER(IntegerOverflowUndef)

test/Analysis/integer-overflow.cpp

-// RUN: %clang_cc1 -Wno-unused-value -Wno-integer-overflow -Wno-constant-conversion -analyze -analyzer-checker=alpha.different.IntegerOverflow,alpha.security.taint,core.DivideZero,deadcode,core.builtin %s -verify
-#define SHRT_MAX ((short)(~0U>>1))
-#define INT_MAX ((int)(~0U>>1))
+// RUN: %clang_cc1 -Wno-unused-value -Wno-integer-overflow -Wno-constant-conversion -analyze -analyzer-checker=alpha.different.IntegerOverflow,alpha.undefbehavior.IntegerOverflow,alpha.security.taint,core.DivideZero,deadcode,core.builtin %s -verify
+#include "Inputs/system-header-simulator.h"
+
+#define SHRT_MAX ((short)(~0U >> 1))
+#define INT_MAX ((int)(~0U >> 1))
 #define INT_MIN (-INT_MAX - 1)
 #define UINT_MAX (~0U)
-#define LONG_MAX ((long)(~0UL>>1))
+#define LONG_MAX ((long)(~0UL >> 1))
 #define LONG_MIN (-LONG_MAX - 1)
 #define ULONG_MAX (~0UL)
-#define LLONG_MAX ((long long)(~0ULL>>1))
+#define LLONG_MAX ((long long)(~0ULL >> 1))
 #define LLONG_MIN (-LLONG_MAX - 1)
 #define ULLONG_MAX (~0ULL)
 
+char *strchr(const char *s, int c);
 int randomInt();
 
 // Addition : signed
 void signAddEW_1(void) {
-  INT_MAX + 1; // expected-warning{{Integer overflow}}
+  INT_MAX + 1; // expected-warning{{Undefined behavior: Integer Overflow. Addition of 2147483647 S32b ((int)(~0U >> 1)) with 1 S32b}}
 }
 void signAddEW_2(void) {
-  INT_MIN + INT_MIN; // expected-warning{{Integer overflow}}
+  INT_MIN + INT_MIN; // expected-warning{{Undefined behavior: Integer Underflow. Addition of -2147483648 S32b (-((int)(~0U >> 1)) - 1) with -2147483648 S32b (-((int)(~0U >> 1)) - 1)}}
 }
 void signAddEW_3(void) {
-  LONG_MAX + 1; // expected-warning{{Integer overflow}}
+  LONG_MAX + 1; // expected-warning{{Undefined behavior: Integer Overflow. Addition of 9223372036854775807 S64b ((long)(~0UL >> 1)) with 1 S64b}}
 }
 void signAddNW_4(void) {
   SHRT_MAX + 1; // no-warning

 void signAddNW_5(int b) {
   if (b > INT_MAX)
     b + 3; // no-warning
-  else if (b == INT_MAX)
-    b + 3; // no-warning
 }
 void signAddEW_6(void) {
   int a = randomInt();
   if (a == INT_MAX)
-    a + 2; // expected-warning{{Integer overflow}}
+    a + 2; // expected-warning{{Undefined behavior: Integer Overflow. Addition of 2147483647 S32b (a) with 2 S32b}}
   else if (a < INT_MAX)
     a + 2; // no-warning
 }
 
 // Addition : unsigned
 void unsignAddEW_1(void) {
-  UINT_MAX + 1; // expected-warning{{Integer overflow}}
+  UINT_MAX + 1; // expected-warning{{Integer Overflow. Addition of 4294967295 U32b (~0U) with 1 U32b}}
 }
 void unsignAddEW_2(void) {
-  1 + (unsigned)-1; // expected-warning{{Integer overflow}}
+  1 + (unsigned)-1; // expected-warning{{Integer Overflow. Addition of 1 U32b with 4294967295 U32b ((unsigned int)-1)}}
 }
 void unsignAddEW_3(void) {
-  ULONG_MAX + 1; // expected-warning{{Integer overflow}}
+  ULONG_MAX + 1; // expected-warning{{Integer Overflow. Addition of 18446744073709551615 U64b (~0UL) with 1 U64b}}
 }
 
 // Subtraction : signed
 void signSubEW_1(void) {
-  INT_MIN - 1; // expected-warning{{Integer overflow}}
+  INT_MIN - 1; // expected-warning{{Undefined behavior: Integer Underflow. Subtraction of 1 S32b from -2147483648 S32b (-((int)(~0U >> 1)) - 1)}}
 }
 void signSubEW_2(void) {
-  -INT_MAX - 2; // expected-warning{{Integer overflow}}
+  -INT_MAX - 2; // expected-warning{{Undefined behavior: Integer Underflow. Subtraction of 2 S32b from -2147483647 S32b (-((int)(~0U >> 1)))}}
 }
 void signSubNW_3(void) {
   -INT_MAX - 1; // no-warning
 }
 void signSubEW_4(void) {
-  LONG_MIN - 1; // expected-warning{{Integer overflow}}
+  LONG_MIN - 1; // expected-warning{{Undefined behavior: Integer Underflow. Subtraction of 1 S64b from -9223372036854775808 S64b (-((long)(~0UL >> 1)) - 1)}}
 }
 
 // Subtraction : unsigned

 }
 void unsignSubEW_2(void) {
   int a = 0;
-  a - (unsigned)1; // expected-warning{{Integer overflow}}
+  a - (unsigned)1; // expected-warning{{Integer Underflow. Subtraction of 1 U32b from 0 U32b (a)}}
 }
 
 // Multiplication : signed
 void signMulEW_1(void) {
-  (INT_MAX / 2) * 3; // expected-warning{{Integer overflow}}
+  (INT_MAX / 2) * 3; // expected-warning{{Undefined behavior: Integer Overflow. Multiplication of 1073741823 S32b (((int)(~0U >> 1)) / 2) with 3 S32b}}
 }
 void signMulNW_2(void) {
   INT_MAX * 0; // no-warning

   0 * INT_MAX; // no-warning
 }
 void signMulEW_4(void) {
-  INT_MIN * (-1); // expected-warning{{Integer overflow}}
+  INT_MIN *(-1); // expected-warning{{Undefined behavior: Integer Overflow. Multiplication of -2147483648 S32b (-((int)(~0U >> 1)) - 1) with -1 S32b}}
 }
 void signMulEW_5(void) {
-  (LONG_MAX / 2) * 3; // expected-warning{{Integer overflow}}
+  (LONG_MAX / 2) * 3; // expected-warning{{Undefined behavior: Integer Overflow. Multiplication of 4611686018427387903 S64b (((long)(~0UL >> 1)) / 2) with 3 S64b}}
 }
 
 // Multiplication : unsigned
 void unsignMulEW_1(void) {
-  (UINT_MAX / 2) * 3; // expected-warning{{Integer overflow}}
+  (UINT_MAX / 2) * 3; // expected-warning{{Integer Overflow. Multiplication of 2147483647 U32b ((~0U) / 2) with 3 U32b}}
 }
 void unsignMulEW_2(void) {
-  (ULONG_MAX / 2) * 3; // expected-warning{{Integer overflow}}
+  (ULONG_MAX / 2) * 3; // expected-warning{{Integer Overflow. Multiplication of 9223372036854775807 U64b ((~0UL) / 2) with 3 U64b}}
 }
 
 // New
 void newEW_1(void) {
   // (INT_MAX / 2) * sizeof(int). Overflowed value is used in memory allocation.
-  new int[INT_MAX / 2]; // expected-warning{{Integer overflow}}
+  new int[INT_MAX / 2]; // expected-warning{{Integer Overflow. Multiplication of 4 U32b with 1073741823 S32b (((int)(~0U >> 1)) / 2) while memory allocation}}
+}
+
+// Test cases for GlobalsMembersHeuristics
+namespace HT_1 {
+void test_1(int b) {
+  if (b == INT_MIN)
+    b - 1; // no-warning
+}
+}
+
+namespace HT_2 {
+class C {
+  int a;
+  void foo() {
+    if (a == INT_MIN)
+      a - 1; // no-warning
+  }
+};
+}
+
+namespace HT_3 {
+class C {
+public:
+  int a;
+};
+void foo() {
+  C c;
+  c.a = INT_MAX;
+  c.a + 1; // no-warning
+}
+}
+
+namespace HT_4 {
+class C {
+  int a;
+  void foo() {
+    a = INT_MAX;
+    ((a - 1) + 1) + 1; // no-warning
+  }
+};
+}
+
+namespace HT_5 {
+class C {
+  int a;
+  void foo() {
+    a = -1;
+    a + 1U; // no-warning
+  }
+};
+}
+
+void conjTest(const char *no_proxy) {
+  unsigned a = 0;
+  if (strchr(", ", no_proxy[0]))
+    a++;
+  // FIXME: shouldn't warn
+  if (strchr(", ", no_proxy[0]))
+    a - 1; // expected-warning{{Integer Underflow. Subtraction of 1 U32b from 0 U32b (a)}}
 }