From 190e93e5dc962cf808affd954043bc489e2412a4 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 28 Oct 2016 16:15:54 +0100
Subject: [PATCH] Check static array bounds, even when the underlying object is
 accessed via a pointer.

---
 src/analyses/goto_check.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 457ec4089f4..07c64c202b3 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1185,13 +1185,11 @@ void goto_checkt::bounds_check(
 
     add_guarded_claim(
       precond,
-      name+" upper bound",
+      name+" dynamic object upper bound",
       "array bounds",
       expr.find_source_location(),
       expr,
       guard);
-
-    return;
   }
 
   const exprt &size=array_type.id()==ID_array ?