rename index_type and enum_constant_type

src/analyses/local_may_alias.cpp

@@ -217,7 +217,7 @@ void local_may_aliast::get_rec(
       if(index_expr.array().id()==ID_symbol)
       {
         index_exprt tmp1=index_expr;
-        tmp1.index()=from_integer(0, index_type());
+        tmp1.index() = from_integer(0, c_index_type());
         address_of_exprt tmp2(tmp1);
         unsigned object_nr=objects.number(tmp2);
         dest.insert(object_nr);
@@ -229,7 +229,7 @@ void local_may_aliast::get_rec(
       else if(index_expr.array().id()==ID_string_constant)
       {
         index_exprt tmp1=index_expr;
-        tmp1.index()=from_integer(0, index_type());
+        tmp1.index() = from_integer(0, c_index_type());
         address_of_exprt tmp2(tmp1);
         unsigned object_nr=objects.number(tmp2);
         dest.insert(object_nr);

src/ansi-c/ansi_c_entry_point.cpp

@@ -448,7 +448,7 @@ bool generate_ansi_c_start_function(
 
         {
           index_exprt index_expr(
-            argv_symbol.symbol_expr(), from_integer(0, index_type()));
+            argv_symbol.symbol_expr(), from_integer(0, c_index_type()));
 
           // disable bounds check on that one
           index_expr.set(ID_C_bounds_check, false);
@@ -466,7 +466,7 @@ bool generate_ansi_c_start_function(
           const symbolt &envp_symbol=ns.lookup("envp'");
 
           index_exprt index_expr(
-            envp_symbol.symbol_expr(), from_integer(0, index_type()));
+            envp_symbol.symbol_expr(), from_integer(0, c_index_type()));
 
           const pointer_typet &pointer_type =
             to_pointer_type(parameters[2].type());

src/ansi-c/c_typecast.cpp

@@ -722,7 +722,7 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
 
   if(src_type.id()==ID_array)
   {
-    index_exprt index(expr, from_integer(0, index_type()));
+    index_exprt index(expr, from_integer(0, c_index_type()));
     expr = typecast_exprt::conditional_cast(address_of_exprt(index), dest_type);
     return;
   }

src/ansi-c/c_typecheck_expr.cpp

@@ -1185,7 +1185,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   }
   else if(op_type.id()==ID_array)
   {
-    index_exprt index(op, from_integer(0, index_type()));
+    index_exprt index(op, from_integer(0, c_index_type()));
     op=address_of_exprt(index);
   }
   else if(op_type.id()==ID_empty)
@@ -1245,7 +1245,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
 
 void c_typecheck_baset::make_index_type(exprt &expr)
 {
-  implicit_typecast(expr, index_type());
+  implicit_typecast(expr, c_index_type());
 }
 
 void c_typecheck_baset::typecheck_expr_index(exprt &expr)
@@ -1456,7 +1456,7 @@ void c_typecheck_baset::typecheck_expr_ptrmember(exprt &expr)
   if(op0_type.id() == ID_array)
   {
     // a->f is the same as a[0].f
-    exprt zero=from_integer(0, index_type());
+    exprt zero = from_integer(0, c_index_type());
     index_exprt index_expr(op, zero, op0_type.subtype());
     index_expr.set(ID_C_lvalue, true);
     op.swap(index_expr);
@@ -1774,7 +1774,7 @@ void c_typecheck_baset::typecheck_expr_dereference(exprt &expr)
     // *a is the same as a[0]
     expr.id(ID_index);
     expr.type()=op_type.subtype();
-    expr.copy_to_operands(from_integer(0, index_type()));
+    expr.copy_to_operands(from_integer(0, c_index_type()));
     assert(expr.operands().size()==2);
   }
   else if(op_type.id()==ID_pointer)

src/ansi-c/c_typecheck_gcc_polymorphic_builtins.cpp

@@ -1445,7 +1445,7 @@ exprt c_typecheck_baset::typecheck_shuffle_vector(
     for(std::size_t i = 0; i < indices_size; ++i)
     {
       // only the least significant bits of each mask element are considered
-      mod_exprt mod_index{index_exprt{indices, from_integer(i, index_type())},
+      mod_exprt mod_index{index_exprt{indices, from_integer(i, c_index_type())},
                           size};
       mod_index.add_source_location() = source_location;
       operands.push_back(std::move(mod_index));

src/ansi-c/c_typecheck_initializer.cpp

@@ -542,7 +542,7 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
         if(current_symbol.is_static_lifetime)
         {
           byte_update_exprt byte_update =
-            make_byte_update(*dest, from_integer(0, index_type()), *zero);
+            make_byte_update(*dest, from_integer(0, c_index_type()), *zero);
           byte_update.add_source_location() = value.source_location();
           *dest = std::move(byte_update);
           dest = &(to_byte_update_expr(*dest).op2());
@@ -1029,7 +1029,7 @@ exprt c_typecheck_baset::do_initializer_list(
     // make complete by setting array size
     size_t size=result.operands().size();
     result.type().id(ID_array);
-    result.type().set(ID_size, from_integer(size, index_type()));
+    result.type().set(ID_size, from_integer(size, c_index_type()));
   }
 
   return result;

src/ansi-c/c_typecheck_type.cpp

@@ -1011,7 +1011,7 @@ void c_typecheck_baset::typecheck_compound_body(
 
         // make it zero-length
         c_type.id(ID_array);
-        c_type.set(ID_size, from_integer(0, index_type()));
+        c_type.set(ID_size, from_integer(0, c_index_type()));
       }
     }
   }

src/ansi-c/literals/convert_string_literal.cpp

@@ -127,7 +127,7 @@ exprt convert_string_literal(const std::string &src)
     result.set(ID_C_string_constant, true);
     result.type()=typet(ID_array);
     result.type().subtype()=subtype;
-    result.type().set(ID_size, from_integer(value.size(), index_type()));
+    result.type().set(ID_size, from_integer(value.size(), c_index_type()));
 
     result.operands().resize(value.size());
     for(std::size_t i=0; i<value.size(); i++)

src/cpp/cpp_constructor.cpp

@@ -97,7 +97,7 @@ optionalt<codet> cpp_typecheckt::cpp_constructor(
       {
         exprt::operandst tmp_operands;
 
-        exprt constant=from_integer(i, index_type());
+        exprt constant = from_integer(i, c_index_type());
         constant.add_source_location()=source_location;
 
         index_exprt index(object, constant);

src/cpp/cpp_destructor.cpp

@@ -56,7 +56,7 @@ optionalt<codet> cpp_typecheckt::cpp_destructor(
     // for each element of the array, call the destructor
     for(mp_integer i=0; i < s; ++i)
     {
-      exprt constant=from_integer(i, index_type());
+      exprt constant = from_integer(i, c_index_type());
       constant.add_source_location()=source_location;
 
       index_exprt index(object, constant);

src/cpp/cpp_typecheck_constructor.cpp

@@ -90,7 +90,7 @@ static void copy_array(
   exprt &block)
 {
   // Build the index expression
-  const exprt constant = from_integer(i, index_type());
+  const exprt constant = from_integer(i, c_index_type());
 
   const cpp_namet array(member_base_name, source_location);
 

src/cpp/cpp_typecheck_conversions.cpp

@@ -80,9 +80,7 @@ bool cpp_typecheckt::standard_conversion_array_to_pointer(
 {
   assert(expr.type().id()==ID_array);
 
-  index_exprt index(
-    expr,
-    from_integer(0, index_type()));
+  index_exprt index(expr, from_integer(0, c_index_type()));
 
   index.set(ID_C_lvalue, true);
 

src/cpp/cpp_typecheck_expr.cpp

@@ -256,9 +256,9 @@ void cpp_typecheckt::typecheck_expr_trinary(if_exprt &expr)
     {
       // array-to-pointer conversion
 
-      index_exprt index1(expr.op1(), from_integer(0, index_type()));
+      index_exprt index1(expr.op1(), from_integer(0, c_index_type()));
 
-      index_exprt index2(expr.op2(), from_integer(0, index_type()));
+      index_exprt index2(expr.op2(), from_integer(0, c_index_type()));
 
       address_of_exprt addr1(index1);
       address_of_exprt addr2(index2);

src/cpp/cpp_typecheck_initializer.cpp

@@ -244,7 +244,7 @@ void cpp_typecheckt::zero_initializer(
     for(mp_integer i=0; i<size; ++i)
     {
       index_exprt index(
-        object, from_integer(i, index_type()), array_type.subtype());
+        object, from_integer(i, c_index_type()), array_type.subtype());
       zero_initializer(index, array_type.subtype(), source_location, ops);
     }
   }

src/goto-instrument/function.cpp

@@ -67,7 +67,7 @@ code_function_callt function_to_call(
     symbol_exprt(s_it->second.name, s_it->second.type),
     {typecast_exprt(
       address_of_exprt(
-        index_exprt(function_id_string, from_integer(0, index_type()))),
+        index_exprt(function_id_string, from_integer(0, c_index_type()))),
       to_code_type(s_it->second.type).parameters()[0].type())});
 
   return call;

src/goto-programs/builtin_functions.cpp

@@ -260,7 +260,7 @@ void goto_convertt::do_scanf(
               const address_of_exprt rhs(
                 index_exprt(
                   tmp_symbol.symbol_expr(),
-                  from_integer(0, index_type())));
+                  from_integer(0, c_index_type())));
 
               // now use array copy
               codet array_copy_statement;
@@ -274,7 +274,7 @@ void goto_convertt::do_scanf(
               copy(array_copy_statement, OTHER, dest);
               #else
               const index_exprt new_lhs(
-                dereference_exprt{ptr}, from_integer(0, index_type()));
+                dereference_exprt{ptr}, from_integer(0, c_index_type()));
               const side_effect_expr_nondett rhs(
                 type->subtype(), function.source_location());
               code_assignt assign(new_lhs, rhs);
@@ -605,7 +605,7 @@ exprt make_va_list(const exprt &expr)
   while(result.type().id() == ID_array &&
         to_array_type(result.type()).size().is_one())
   {
-    result = index_exprt{result, from_integer(0, index_type())};
+    result = index_exprt{result, from_integer(0, c_index_type())};
   }
 
   return result;
@@ -704,8 +704,8 @@ void goto_convertt::do_havoc_slice(
 
   const symbolt &nondet_contents =
     new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
-  const exprt &nondet_contents_expr = address_of_exprt{
-    index_exprt{nondet_contents.symbol_expr(), from_integer(0, index_type())}};
+  const exprt &nondet_contents_expr = address_of_exprt{index_exprt{
+    nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
 
   const exprt &arg0 =
     typecast_exprt::conditional_cast(arguments[0], pointer_type(empty_typet{}));

src/goto-programs/goto_convert_side_effect.cpp

@@ -214,7 +214,7 @@ void goto_convertt::remove_pre(
   typet constant_type;
 
   if(op_type.id() == ID_pointer)
-    constant_type = index_type();
+    constant_type = c_index_type();
   else if(is_number(op_type))
     constant_type = op_type;
   else
@@ -300,7 +300,7 @@ void goto_convertt::remove_post(
   typet constant_type;
 
   if(op_type.id() == ID_pointer)
-    constant_type = index_type();
+    constant_type = c_index_type();
   else if(is_number(op_type))
     constant_type = op_type;
   else

src/goto-programs/goto_instruction_code.cpp

@@ -34,7 +34,7 @@ code_inputt::code_inputt(
   optionalt<source_locationt> location)
   : code_inputt{{address_of_exprt(index_exprt(
                    string_constantt(description),
-                   from_integer(0, index_type()))),
+                   from_integer(0, c_index_type()))),
                  std::move(expression)},
                 std::move(location)}
 {
@@ -62,7 +62,7 @@ code_outputt::code_outputt(
   optionalt<source_locationt> location)
   : code_outputt{{address_of_exprt(index_exprt(
                     string_constantt(description),
-                    from_integer(0, index_type()))),
+                    from_integer(0, c_index_type()))),
                   std::move(expression)},
                  std::move(location)}
 {

src/goto-programs/graphml_witness.cpp

@@ -109,9 +109,7 @@ std::string graphml_witnesst::convert_assign_rec(
     forall_operands(it, assign.rhs())
     {
       index_exprt index(
-        assign.lhs(),
-        from_integer(i++, index_type()),
-        type.subtype());
+        assign.lhs(), from_integer(i++, c_index_type()), type.subtype());
       if(!result.empty())
         result+=' ';
       result+=convert_assign_rec(identifier, code_assignt(index, *it));

src/goto-programs/rewrite_union.cpp

@@ -82,14 +82,14 @@ void rewrite_union(exprt &expr)
 
     if(op.type().id() == ID_union_tag || op.type().id() == ID_union)
     {
-      exprt offset=from_integer(0, index_type());
+      exprt offset = from_integer(0, c_index_type());
       expr = make_byte_extract(op, offset, expr.type());
     }
   }
   else if(expr.id()==ID_union)
   {
     const union_exprt &union_expr=to_union_expr(expr);
-    exprt offset=from_integer(0, index_type());
+    exprt offset = from_integer(0, c_index_type());
     side_effect_expr_nondett nondet(expr.type(), expr.source_location());
     expr = make_byte_update(nondet, offset, union_expr.op());
   }

src/goto-programs/string_abstraction.cpp

@@ -573,7 +573,7 @@ void string_abstractiont::abstract_function_call(
         str_args.back().type().subtype() == abstract_type.subtype(),
         "argument array type differs from formal parameter pointer type");
 
-      index_exprt idx(str_args.back(), from_integer(0, index_type()));
+      index_exprt idx(str_args.back(), from_integer(0, c_index_type()));
       // disable bounds check on that one
       idx.set(ID_C_bounds_check, false);
 

src/goto-programs/string_instrumentation.cpp

@@ -394,7 +394,7 @@ void string_instrumentationt::do_format_string_read(
 
           if(arg.type().id() != ID_pointer)
           {
-            index_exprt index(temp, from_integer(0, index_type()));
+            index_exprt index(temp, from_integer(0, c_index_type()));
             temp=address_of_exprt(index);
           }
 
@@ -437,7 +437,7 @@ void string_instrumentationt::do_format_string_read(
 
         if(arg.type().id() != ID_pointer)
         {
-          index_exprt index(temp, from_integer(0, index_type()));
+          index_exprt index(temp, from_integer(0, c_index_type()));
           temp=address_of_exprt(index);
         }
 
@@ -778,9 +778,7 @@ void string_instrumentationt::do_strerror(
 
   // return a pointer to some magic buffer
   index_exprt index(
-    symbol_buf.symbol_expr(),
-    from_integer(0, index_type()),
-    char_type());
+    symbol_buf.symbol_expr(), from_integer(0, c_index_type()), char_type());
 
   address_of_exprt ptr(index);
 
@@ -843,7 +841,7 @@ void string_instrumentationt::invalidate_buffer(
   else
   {
     index_exprt index(
-      buffer, from_integer(0, index_type()), buf_type.subtype());
+      buffer, from_integer(0, c_index_type()), buf_type.subtype());
     bufp=address_of_exprt(index);
   }
 

src/goto-symex/goto_symex.cpp

@@ -267,7 +267,7 @@ void goto_symext::assign_string_constant(
     "symbol shall have value derived from char array content");
 
   const address_of_exprt string_data(
-    index_exprt(aux_symbol.symbol_expr(), from_integer(0, index_type())));
+    index_exprt(aux_symbol.symbol_expr(), from_integer(0, c_index_type())));
 
   symex_assign.assign_symbol(char_array, expr_skeletont{}, string_data, {});
 

src/goto-symex/symex_clean_expr.cpp

@@ -45,7 +45,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
     {
       byte_extract_exprt be = make_byte_extract(
         if_expr.false_case(),
-        from_integer(0, index_type()),
+        from_integer(0, c_index_type()),
         if_expr.true_case().type());
 
       if_expr.false_case().swap(be);
@@ -93,7 +93,7 @@ process_array_expr(exprt &expr, bool do_simplify, const namespacet &ns)
           simplify(array_size.value(), ns);
         expr = make_byte_extract(
           expr,
-          from_integer(0, index_type()),
+          from_integer(0, c_index_type()),
           array_typet(char_type(), array_size.value()));
       }