Index: clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
+++ clang/lib/StaticAnalyzer/Checkers/ContainerModeling.cpp
@@ -47,6 +47,8 @@
                  SVal Cont, SVal RetVal) const;
   void handleEmpty(CheckerContext &C, const Expr *CE, const Expr *ContE,
                    SVal Cont, SVal RetVal) const;
+  void handleSize(CheckerContext &C, const Expr *CE, const Expr *ContE,
+                  SVal Cont, SVal RetVal) const;
   void handleAssign(CheckerContext &C, const Expr *CE, const Expr *ContE,
                     SVal Cont, SVal RetVal) const;
   void handleClear(CheckerContext &C, const Expr *CE, const Expr *ContE,
@@ -102,6 +104,7 @@
 
     // Capacity
     {{0, "empty", 0}, &ContainerModeling::handleEmpty},
+    {{0, "size", 0}, &ContainerModeling::handleSize},
 
     // Modifiers
     {{0, "clear", 0}, &ContainerModeling::handleClear},
@@ -170,6 +173,10 @@
 SymbolRef rebaseSymbol(ProgramStateRef State, SValBuilder &SVB, SymbolRef Expr,
                         SymbolRef OldSym, SymbolRef NewSym);
 bool hasLiveIterators(ProgramStateRef State, const MemRegion *Cont);
+const llvm::APSInt* calculateSize(ProgramStateRef State, SymbolRef Begin,
+                                  SymbolRef End);
+ProgramStateRef ensureNonNegativeSize(ProgramStateRef State,
+                                      const MemRegion *Cont);
 
 } // namespace
 
@@ -446,6 +453,72 @@
   }
 }
 
+void ContainerModeling::handleSize(CheckerContext &C, const Expr *CE,
+                                   const Expr *, SVal Cont, SVal RetVal) const {
+  const auto *ContReg = Cont.getAsRegion();
+  if (!ContReg)
+    return;
+
+  ContReg = ContReg->getMostDerivedObjectRegion();
+
+  auto State = C.getState();
+
+  State = createContainerBegin(State, ContReg, CE, C.getASTContext().LongTy,
+                               C.getLocationContext(), C.blockCount());
+  auto BeginSym = getContainerBegin(State, ContReg);
+  State = createContainerEnd(State, ContReg, CE, C.getASTContext().LongTy,
+                             C.getLocationContext(), C.blockCount());
+  auto EndSym = getContainerEnd(State, ContReg);
+  const llvm::APSInt *CalcSize = calculateSize(State, BeginSym, EndSym);
+
+  auto &SVB = C.getSValBuilder();
+  auto &BVF = State->getBasicVals();
+  const llvm::APSInt *RetSize = nullptr;
+  if (const auto *KnownSize = SVB.getKnownValue(State, RetVal)) {
+    RetSize = &BVF.Convert(C.getASTContext().LongTy, *KnownSize);
+  }
+
+  if (RetSize) {
+    // If the return value is a concrete integer, then try to adjust the size
+    // of the container (the difference between its `begin()` and `end()` to
+    // this size. Function `relateSymbols()` returns null if it contradits
+    // the current size.
+    const auto CalcEnd =
+      SVB.evalBinOp(State, BO_Add, nonloc::SymbolVal(BeginSym),
+                    nonloc::ConcreteInt(*RetSize), C.getASTContext().LongTy)
+      .getAsSymbol();
+    if (CalcEnd) {
+      State = relateSymbols(State, EndSym, CalcEnd, true);
+    }
+  } else {
+    if (CalcSize) {
+      // If the current size is a concrete integer, bind this to the return
+      // value of the function instead of the current one.
+      auto CSize = nonloc::ConcreteInt(BVF.Convert(CE->getType(), *CalcSize));
+      State = State->BindExpr(CE, C.getLocationContext(), CSize);
+    } else {
+      // If neither the returned nor the current size is a concrete integer,
+      // replace the return value with the symbolic difference of the
+      // container's `begin()` and `end()` symbols.
+      auto Size = SVB.evalBinOp(State, BO_Sub, nonloc::SymbolVal(EndSym),
+                                nonloc::SymbolVal(BeginSym),
+                                C.getASTContext().LongTy);
+      if (Size.isUnknown())
+        return;
+
+      auto CastedSize = SVB.evalCast(Size, CE->getType(),
+                                     C.getASTContext().LongTy);
+      State = State->BindExpr(CE, C.getLocationContext(), CastedSize);
+    }
+  }
+
+  if (State) {
+    C.addTransition(State);
+  } else {
+    C.generateSink(State, C.getPredecessor());
+  }
+}
+
 void ContainerModeling::handleAssign(CheckerContext &C, const Expr *CE,
                                      const Expr *, SVal Cont,
                                      SVal RetVal) const {
@@ -932,7 +1005,8 @@
 
   if (CDataPtr) {
     const auto CData = CDataPtr->newBegin(Sym);
-    return setContainerData(State, Cont, CData);
+    State = setContainerData(State, Cont, CData);
+    return ensureNonNegativeSize(State, Cont);
   }
 
   const auto CData = ContainerData::fromBegin(Sym);
@@ -955,7 +1029,8 @@
 
   if (CDataPtr) {
     const auto CData = CDataPtr->newEnd(Sym);
-    return setContainerData(State, Cont, CData);
+    State = setContainerData(State, Cont, CData);
+    return ensureNonNegativeSize(State, Cont);
   }
 
   const auto CData = ContainerData::fromEnd(Sym);
@@ -1129,6 +1204,63 @@
   return false;
 }
 
+const llvm::APSInt* calculateSize(ProgramStateRef State, SymbolRef Begin,
+                                  SymbolRef End) {
+  if (!Begin || !End)
+    return nullptr;
+
+  auto &SVB = State->getStateManager().getSValBuilder();
+  auto &SymMgr = State->getSymbolManager();
+  auto Size = SVB.evalBinOp(State, BO_Sub, nonloc::SymbolVal(End),
+                            nonloc::SymbolVal(Begin),
+                            SymMgr.getType(End)).getAsSymbol();
+  if (!Size)
+    return nullptr;
+
+  llvm::APSInt Diff = llvm::APSInt::get(0);
+  if (const auto *SizeExpr = dyn_cast<SymIntExpr>(Size)) {
+    assert(BinaryOperator::isAdditiveOp(SizeExpr->getOpcode()) &&
+           "Symbolic positions must be additive expressions");
+    if (SizeExpr->getOpcode() == BO_Add) {
+      Diff = SizeExpr->getRHS();
+    } else {
+      Diff = -SizeExpr->getRHS();
+    }
+    Size = SizeExpr->getLHS();
+  }
+
+  auto &CM = State->getConstraintManager();
+  if (const auto *SizeInt = CM.getSymVal(State, Size)) {
+    auto &BVF = SymMgr.getBasicVals();
+    return &BVF.getValue(Diff + *SizeInt);
+  }
+
+  return nullptr;
+}
+
+ProgramStateRef ensureNonNegativeSize(ProgramStateRef State,
+                                      const MemRegion *Cont) {
+  const auto *CData = getContainerData(State, Cont);
+  if (!CData)
+    return State;
+
+  SymbolRef BeginSym = CData->getBegin();
+  SymbolRef EndSym = CData->getEnd();
+  if (!BeginSym || !EndSym)
+    return State;
+
+  auto &SVB = State->getStateManager().getSValBuilder();
+  auto NonNegativeSize = SVB.evalBinOp(State, BO_GE,
+                                       nonloc::SymbolVal(EndSym),
+                                       nonloc::SymbolVal(BeginSym),
+                                       SVB.getConditionType())
+    .getAs<DefinedSVal>();
+  assert(NonNegativeSize);
+  State = State->assume(*NonNegativeSize, true);
+  assert(State && "Container size must not be negative.");
+  return State;
+}
+
 } // namespace
 
 void ento::registerContainerModeling(CheckerManager &mgr) {
Index: clang/lib/StaticAnalyzer/Checkers/Iterator.h
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/Iterator.h
+++ clang/lib/StaticAnalyzer/Checkers/Iterator.h
@@ -187,6 +187,8 @@
 assumeComparison(ProgramStateRef State, SymbolRef Sym1, SymbolRef Sym2,
                  DefinedSVal RetVal, OverloadedOperatorKind Op);
 
+ProgramStateRef relateSymbols(ProgramStateRef State, SymbolRef Sym1,
+                              SymbolRef Sym2, bool Equal);
 bool compare(ProgramStateRef State, SymbolRef Sym1, SymbolRef Sym2,
              BinaryOperator::Opcode Opc);
 bool compare(ProgramStateRef State, NonLoc NL1, NonLoc NL2,
Index: clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
+++ clang/lib/StaticAnalyzer/Checkers/Iterator.cpp
@@ -18,9 +18,6 @@
 namespace ento {
 namespace iterator {
 
-ProgramStateRef relateSymbols(ProgramStateRef State, SymbolRef Sym1,
-                              SymbolRef Sym2, bool Equal);
-
 bool isIteratorType(const QualType &Type) {
   if (Type->isPointerType())
     return true;
Index: clang/test/Analysis/container-modeling.cpp
===================================================================
--- clang/test/Analysis/container-modeling.cpp
+++ clang/test/Analysis/container-modeling.cpp
@@ -14,6 +14,7 @@
 void clang_analyzer_denote(long, const char*);
 void clang_analyzer_express(long);
 void clang_analyzer_eval(bool);
+void clang_analyzer_dump(std::size_t);
 void clang_analyzer_warnIfReached();
 
 extern void __assert_fail (__const char *__assertion, __const char *__file,
@@ -104,6 +105,125 @@
   // expected-note@-3   {{FALSE}}
 }
 
+// size()
+
+void size0(const std::vector<int>& V) {
+  assert(V.size() == 0); // expected-note 2{{'?' condition is true}}
+                         // expected-note@-1 2{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{TRUE}}
+  // expected-note@-3   {{TRUE}}
+
+  clang_analyzer_dump(V.size()); // expected-warning{{0}}
+                                 // expected-note@-1{{0}}
+}
+
+void size1(const std::vector<int>& V) {
+  assert(V.size() == 1); // expected-note 2{{'?' condition is true}}
+                         // expected-note@-1 2{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 1);
+  // expected-warning@-2{{TRUE}}
+  // expected-note@-3   {{TRUE}}
+
+  clang_analyzer_dump(V.size()); // expected-warning{{1}}
+                                 // expected-note@-1{{1}}
+}
+
+void size2(std::vector<int>& V) {
+  assert(V.size() == 1); // expected-note 2{{'?' condition is true}}
+                         // expected-note@-1 2{{Assuming the condition is true}}
+
+  V.push_back(1);
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 2);
+  // expected-warning@-2{{TRUE}}
+  // expected-note@-3   {{TRUE}}
+
+  clang_analyzer_dump(V.size()); // expected-warning{{2}}
+                                 // expected-note@-1{{2}}
+}
+
+void size3(std::vector<int>& V) {
+  assert(V.size() <= 10); // expected-note 6{{'?' condition is true}}
+                         // expected-note@-1 6{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) + 1 ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4  {{Assuming the condition is true}}
+  // expected-note@-5 4{{Assuming the condition is false}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 10);
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4  {{Assuming the condition is true}}
+  // expected-note@-5 2{{Assuming the condition is false}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 11);
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+}
+
+void size4(std::vector<int>& V) {
+  assert(V.size() >= 10); // expected-note 6{{'?' condition is true}}
+                         // expected-note@-1 6{{Assuming the condition is true}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) + 1 ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V));
+  // expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{FALSE}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 10);
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4  {{Assuming the condition is true}}
+  // expected-note@-5 3{{Assuming the condition is false}}
+
+  clang_analyzer_eval(clang_analyzer_container_end(V) ==
+                      clang_analyzer_container_begin(V) + 11);
+  // expected-warning@-2{{TRUE}} expected-warning@-2{{FALSE}}
+  // expected-note@-3   {{TRUE}} expected-note@-3   {{FALSE}}
+  // expected-note@-4{{Assuming the condition is true}}
+  // expected-note@-5{{Assuming the condition is false}}
+}
+
+void size5(std::vector<int>& V) {
+  long s = V.size();
+
+  clang_analyzer_denote(clang_analyzer_container_begin(V), "$V.begin()");
+  clang_analyzer_denote(clang_analyzer_container_end(V), "$V.end()");
+  
+  V.push_back(1);
+
+  clang_analyzer_express(V.size());
+  // expected-warning@-1{{$V.end() - $V.begin() + 1}}
+  // expected-note@-2   {{$V.end() - $V.begin() + 1}}
+  clang_analyzer_express(s + 1);
+  // expected-warning@-1{{$V.end() - $V.begin() + 1}}
+  // expected-note@-2   {{$V.end() - $V.begin() + 1}}
+  clang_analyzer_eval(V.size() == s + 1); // expected-warning{{TRUE}}
+                                          // expected-note@-1{{TRUE}}
+}
+
 ////////////////////////////////////////////////////////////////////////////////
 ///
 /// C O N T A I N E R   M O D I F I E R S