Warning for when bounds declarations are not provably true.

include/clang/Basic/DiagnosticSemaKinds.td

@@ -9351,6 +9351,17 @@ def err_bounds_type_annotation_lost_checking : Error<
   def err_bounds_cast_error_with_array_syntax
       : Error<"invalid bounds cast: expected _Array_ptr type">;
 
+  def warn_bounds_declaration_not_true : Warning<
+    "bounds declaration for '%0' may not be true after assignment">,
+    DefaultIgnore,
+    InGroup<DiagGroup<"check-bounds-decls">>;
+
+  def note_declared_bounds_for_expr : Note<
+    "declared bounds for '%0' are '%1'">;
+
+  def note_inferred_bounds_for_expr : Note<
+    "inferred bounds for right-hand side are '%0'">;
+
 } // end of Checked C Category
 
 } // end of sema component.

lib/Sema/SemaBounds.cpp

@@ -880,6 +880,33 @@ namespace {
       return false;
     }
 
+    // Given an assignment target = e, where target has declared bounds
+    // DeclaredBounds and and e has inferred bounds SrcBounds, make sure
+    // that SrcBounds implies that DeclaredBounds is provably true.
+    void CheckBoundsDeclIsProvable(SourceLocation ExprLoc, Expr *Target,
+                                   BoundsExpr *DeclaredBounds, Expr *Src,
+                                   BoundsExpr *SrcBounds) {
+      if (S.Diags.isIgnored(diag::warn_bounds_declaration_not_true, ExprLoc))
+        return;
+
+      // source bounds(any) implies that any other bounds is valid.
+      if (SrcBounds->isAny())
+        return;
+
+      // target bounds(none) implied by any other bounds.
+      if (DeclaredBounds->isNone())
+        return;
+
+      if (!S.Context.EquivalentBounds(DeclaredBounds, SrcBounds)) {
+         S.Diag(ExprLoc, diag::warn_bounds_declaration_not_true) << Target
+          << Target->getSourceRange() << Src->getSourceRange();
+         S.Diag(Target->getExprLoc(), diag::note_declared_bounds_for_expr) <<
+           Target << DeclaredBounds << Target->getSourceRange();
+         S.Diag(Src->getExprLoc(), diag::note_inferred_bounds_for_expr) <<
+           SrcBounds << Src->getSourceRange();
+      }
+    }
+
   public:
     CheckBoundsDeclarations(Sema &S) : S(S),
      DumpBounds(S.getLangOpts().DumpInferredBounds) {}
@@ -907,9 +934,13 @@ namespace {
           else
             RHSBounds = S.InferRValueBounds(RHS);
           if (RHSBounds->isNone()) {
-             S.Diag(RHS->getLocStart(), diag::err_expected_bounds_for_assignment) << RHS->getSourceRange();
+             S.Diag(RHS->getLocStart(),
+                    diag::err_expected_bounds_for_assignment)
+                    << RHS->getSourceRange();
              RHSBounds = S.CreateInvalidBoundsExpr();
-          }
+          } else
+            CheckBoundsDeclIsProvable(E->getExprLoc(), LHS, LHSTargetBounds,
+                                      RHS, RHSBounds);
         }
       }
 
@@ -962,7 +993,9 @@ namespace {
         BoundsExpr *SrcBounds =
           S.InferRValueBounds(E->getSubExpr());
         if (SrcBounds->isNone()) {
-          S.Diag(E->getSubExpr()->getLocStart(), diag::err_expected_bounds_for_ptr_cast)  << E->getSubExpr()->getSourceRange();
+          S.Diag(E->getSubExpr()->getLocStart(),
+                 diag::err_expected_bounds_for_ptr_cast)
+                 << E->getSubExpr()->getSourceRange();
           SrcBounds = S.CreateInvalidBoundsExpr();
         }
         assert(SrcBounds);

test/CheckedC/bounds-decl-checking.c

@@ -0,0 +1,16 @@
+// Tests for checking that bounds declarations hold after assignments to
+// variables and initialization of variables.  Because the static checker is
+// mostly unimplemented, we only issue warnings when bounds declarations
+// cannot be provided to hold.
+//
+// RUN: %clang -cc1 -fcheckedc-extension -Wcheck-bounds-decls -verify -verify-ignore-unexpected=note %s
+
+void f1(_Array_ptr<int> p : bounds(p, p + x), int x) {
+    _Array_ptr<int> r : bounds(p, p + x) = 0;
+    r = p;
+}
+
+void f2(_Array_ptr<int> p : count(x), int x) {
+  _Array_ptr<int> r : count(x) = 0;
+  r = p;  // expected-warning {{may not be true}}
+}