index_exprt now requires a type with subtype

This commit adds a precondition to the constructor of index_exprt that
enforces that the type of the 'array' operand has a subtype.

Author: kroening

src/cpp/cpp_constructor.cpp

@@ -100,7 +100,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
         exprt constant = from_integer(i, c_index_type());
         constant.add_source_location()=source_location;
 
-        index_exprt index(object, constant);
+        index_exprt index = index_exprt(object_tc, constant);
         index.add_source_location()=source_location;
 
         if(!operands.empty())

src/util/std_expr.h

@@ -1417,9 +1417,7 @@ class index_exprt:public binary_exprt
         _array,
         ID_index,
         std::move(_index),
-        _array.type().has_subtype()
-          ? to_type_with_subtype(_array.type()).subtype()
-          : typet(ID_nil))
+        to_type_with_subtype(_array.type()).subtype())
   {
   }
 

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -29,8 +29,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
       {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}},
     rowt{
       "Address of index of struct member",
-      {index_exprt{
-         member_exprt{object_base, "baz", unsignedbv_typet{8}}, index},
+      {index_exprt{member_exprt{object_base, "baz", base_type}, index},
        pointer_type}},
     rowt{
       "Address of struct member at index",