Constant array reading from top handled correctly

Author: thk123

src/analyses/variable-sensitivity/constant_array_abstract_object.cpp

@@ -225,26 +225,35 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(
   const index_exprt &index,
   const namespacet &ns) const
 {
-  mp_integer index_value;
-  if(eval_index(index, env, ns, index_value))
+  if(is_top())
   {
-    // Here we are assuming it is always in bounds
-    if(map.find(index_value)==map.cend())
+    return env.abstract_object_factory(
+      index.type(), ns, true);
+  }
+  else
+  {
+    assert(!is_bottom());
+    mp_integer index_value;
+    if(eval_index(index, env, ns, index_value))
     {
-      return env.abstract_object_factory(type().subtype(), ns, true, false);
+      // Here we are assuming it is always in bounds
+      if(map.find(index_value)==map.cend())
+      {
+        return env.abstract_object_factory(type().subtype(), ns, true, false);
+      }
+      else
+      {
+        return map.find(index_value)->second;
+      }
     }
     else
     {
-      return map.find(index_value)->second;
+      // Reading from somewhere in the array
+      // TODO(tkiley): merge all the values of the array, we may be able to
+      // do better than returning top
+      return env.abstract_object_factory(type().subtype(), ns, true, false);
     }
   }
-  else
-  {
-    // Reading from somewhere in the array
-    // TODO(tkiley): merge all the values of the array, we may be able to
-    // do better than returning top
-    return env.abstract_object_factory(type().subtype(), ns, true, false);
-  }
 }
 
 /*******************************************************************\