do not access typet::subtype() without cast to appropriate specialisation

Daniel Kroening · Daniel Kroening · commit bdfe7af88a31 · 2018-10-03T09:24:49.000+01:00
Rationale: not every type has a subtype, and if a type doesn't have one,
then accessing subtype() results in a memory safety violation.  A checked
cast to the right specialisation prevents this.

Eventually, typet::subtype() will be removed to enforce this.
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
@@ -616,8 +616,9 @@ void rw_range_sett::get_objects_rec(const typet &type)
   // TODO should recurse into various composite types
   if(type.id()==ID_array)
   {
-    get_objects_rec(type.subtype());
-    get_objects_rec(get_modet::READ, to_array_type(type).size());
+    const auto &array_type = to_array_type(type);
+    get_objects_rec(array_type.subtype());
+    get_objects_rec(get_modet::READ, array_type.size());
   }
 }
 
diff --git a/src/goto-instrument/thread_instrumentation.cpp b/src/goto-instrument/thread_instrumentation.cpp
@@ -140,5 +140,7 @@ void mutex_init_instrumentation(goto_modelt &goto_model)
 
   Forall_goto_functions(f_it, goto_model.goto_functions)
     mutex_init_instrumentation(
-      goto_model.symbol_table, f_it->second.body, lock_type.subtype());
+      goto_model.symbol_table,
+      f_it->second.body,
+      to_pointer_type(lock_type).subtype());
 }
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
@@ -57,7 +57,7 @@ void goto_symext::initialize_auto_object(
   else if(type.id()==ID_pointer)
   {
     const pointer_typet &pointer_type=to_pointer_type(type);
-    const typet &subtype=ns.follow(type.subtype());
+    const typet &subtype = ns.follow(pointer_type.subtype());
 
     // we don't like function pointers and
     // we don't like void *
@@ -67,7 +67,7 @@ void goto_symext::initialize_auto_object(
       // could be NULL nondeterministically
 
       address_of_exprt address_of_expr(
-        make_auto_object(type.subtype(), state), pointer_type);
+        make_auto_object(pointer_type.subtype(), state), pointer_type);
 
       if_exprt rhs(
         side_effect_expr_nondett(bool_typet(), expr.source_location()),
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -211,7 +211,7 @@ static bool check_renaming(const typet &type)
         return true;
   }
   else if(type.has_subtype())
-    return check_renaming(type.subtype());
+    return check_renaming(to_type_with_subtype(type).subtype());
 
   return false;
 }
@@ -489,7 +489,7 @@ void goto_symex_statet::rename(
   {
     auto &address_of_expr = to_address_of_expr(expr);
     rename_address(address_of_expr.object(), ns, level);
-    expr.type().subtype() = address_of_expr.object().type();
+    to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();
   }
   else
   {
@@ -725,7 +725,7 @@ void goto_symex_statet::rename_address(
 
       rename_address(index_expr.array(), ns, level);
       PRECONDITION(index_expr.array().type().id() == ID_array);
-      expr.type()=index_expr.array().type().subtype();
+      expr.type() = to_array_type(index_expr.array().type()).subtype();
 
       // the index is not an address
       rename(index_expr.index(), ns, level);
@@ -810,8 +810,9 @@ void goto_symex_statet::rename(
 
   if(type.id()==ID_array)
   {
-    rename(type.subtype(), irep_idt(), ns, level);
-    rename(to_array_type(type).size(), ns, level);
+    auto &array_type = to_array_type(type);
+    rename(array_type.subtype(), irep_idt(), ns, level);
+    rename(array_type.size(), ns, level);
   }
   else if(type.id()==ID_struct ||
           type.id()==ID_union ||
@@ -832,7 +833,7 @@ void goto_symex_statet::rename(
   }
   else if(type.id()==ID_pointer)
   {
-    rename(type.subtype(), irep_idt(), ns, level);
+    rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);
   }
   else if(type.id() == ID_symbol_type)
   {
@@ -876,8 +877,9 @@ void goto_symex_statet::get_original_name(typet &type) const
 
   if(type.id()==ID_array)
   {
-    get_original_name(type.subtype());
-    get_original_name(to_array_type(type).size());
+    auto &array_type = to_array_type(type);
+    get_original_name(array_type.subtype());
+    get_original_name(array_type.size());
   }
   else if(type.id()==ID_struct ||
           type.id()==ID_union ||
@@ -894,7 +896,7 @@ void goto_symex_statet::get_original_name(typet &type) const
   }
   else if(type.id()==ID_pointer)
   {
-    get_original_name(type.subtype());
+    get_original_name(to_pointer_type(type).subtype());
   }
 }
 
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
@@ -60,9 +60,11 @@ void goto_symext::symex_allocate(
   const irep_idt &mode = function_symbol->mode;
 
   // is the type given?
-  if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
+  if(
+    code.type().id() == ID_pointer &&
+    to_pointer_type(code.type()).subtype().id() != ID_empty)
   {
-    object_type=code.type().subtype();
+    object_type = to_pointer_type(code.type()).subtype();
   }
   else
   {
@@ -190,11 +192,11 @@ void goto_symext::symex_allocate(
 
   if(object_type.id()==ID_array)
   {
-    index_exprt index_expr(value_symbol.type.subtype());
+    const auto &array_type = to_array_type(object_type);
+    index_exprt index_expr(array_type.subtype());
     index_expr.array()=value_symbol.symbol_expr();
     index_expr.index()=from_integer(0, index_type());
-    rhs=address_of_exprt(
-      index_expr, pointer_type(value_symbol.type.subtype()));
+    rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
   }
   else
   {
@@ -391,6 +393,8 @@ void goto_symext::symex_cpp_new(
 
   PRECONDITION(code.type().id() == ID_pointer);
 
+  const auto &pointer_type = to_pointer_type(code.type());
+
   do_array =
     (code.get(ID_statement) == ID_cpp_new_array ||
      code.get(ID_statement) == ID_java_new_array_data);
@@ -418,19 +422,18 @@ void goto_symext::symex_cpp_new(
   {
     exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
     clean_expr(size_arg, state, false);
-    symbol.type = array_typet(code.type().subtype(), size_arg);
+    symbol.type = array_typet(pointer_type.subtype(), size_arg);
   }
   else
-    symbol.type=code.type().subtype();
+    symbol.type = pointer_type.subtype();
 
   symbol.type.set(ID_C_dynamic, true);
 
   state.symbol_table.add(symbol);
 
   // make symbol expression
 
-  exprt rhs(ID_address_of, code.type());
-  rhs.type().subtype()=code.type().subtype();
+  exprt rhs(ID_address_of, pointer_type);
 
   if(do_array)
   {
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
@@ -321,8 +321,11 @@ void goto_symext::dereference_rec(
     exprt &object=address_of_expr.object();
 
     const typet &expr_type=ns.follow(expr.type());
-    expr=address_arithmetic(object, state, guard,
-                            expr_type.subtype().id()==ID_array);
+    expr = address_arithmetic(
+      object,
+      state,
+      guard,
+      to_pointer_type(expr_type).subtype().id() == ID_array);
   }
   else if(expr.id()==ID_typecast)
   {
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -72,7 +72,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   }
   else if(type_id==ID_c_bit_field)
   {
-    const typet &subtype=type.subtype();
+    const typet &subtype = to_c_bit_field_type(type).subtype();
     if(subtype.id()==ID_signedbv)
     {
       int_value=binary2integer(id2string(value), true);
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
@@ -116,7 +116,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       result = side_effect_expr_nondett(type, source_location);
     else
     {
-      exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
+      exprt sub_zero =
+        expr_initializer_rec(to_complex_type(type).subtype(), source_location);
       result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));
     }
 
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
@@ -124,7 +124,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
      src.id()!=ID_pointer)
   {
     if(src.has_subtype())
-      find_symbols(kind, src.subtype(), dest);
+      find_symbols(kind, to_type_with_subtype(src).subtype(), dest);
 
     forall_subtypes(it, src)
       find_symbols(kind, *it, dest);
diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp
@@ -60,14 +60,14 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
   const auto &id = type.id();
 
   if(id == ID_pointer)
-    return os << '*' << format(type.subtype());
+    return os << '*' << format(to_pointer_type(type).subtype());
   else if(id == ID_array)
   {
     const auto &t = to_array_type(type);
     if(t.is_complete())
-      return os << format(type.subtype()) << '[' << format(t.size()) << ']';
+      return os << format(t.subtype()) << '[' << format(t.size()) << ']';
     else
-      return os << format(type.subtype()) << "[]";
+      return os << format(t.subtype()) << "[]";
   }
   else if(id == ID_struct)
     return format_rec(os, to_struct_type(type));
diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp
@@ -154,7 +154,10 @@ json_objectt json(
   else if(type.id()==ID_c_enum_tag)
   {
     // we return the base type
-    return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
+    return json(
+      to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(type))).subtype(),
+      ns,
+      mode);
   }
   else if(type.id()==ID_fixedbv)
   {
@@ -165,7 +168,7 @@ json_objectt json(
   else if(type.id()==ID_pointer)
   {
     result["name"]=json_stringt("pointer");
-    result["subtype"]=json(type.subtype(), ns, mode);
+    result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);
   }
   else if(type.id()==ID_bool)
   {
@@ -174,12 +177,12 @@ json_objectt json(
   else if(type.id()==ID_array)
   {
     result["name"]=json_stringt("array");
-    result["subtype"]=json(type.subtype(), ns, mode);
+    result["subtype"] = json(to_array_type(type).subtype(), ns, mode);
   }
   else if(type.id()==ID_vector)
   {
     result["name"]=json_stringt("vector");
-    result["subtype"]=json(type.subtype(), ns, mode);
+    result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);
     result["size"]=json(to_vector_type(type).size(), ns, mode);
   }
   else if(type.id()==ID_struct)
@@ -242,9 +245,8 @@ json_objectt json(
         lang=std::unique_ptr<languaget>(get_default_language());
     }
 
-    const typet &underlying_type=
-      type.id()==ID_c_bit_field?type.subtype():
-      type;
+    const typet &underlying_type =
+      type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;
 
     std::string type_string;
     bool error=lang->from_type(underlying_type, type_string, ns);
@@ -270,7 +272,8 @@ json_objectt json(
     {
       result["name"]=json_stringt("integer");
       result["binary"] = json_stringt(constant_expr.get_value());
-      result["width"]=json_numbert(type.subtype().get_string(ID_width));
+      result["width"] =
+        json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));
       result["type"]=json_stringt("enum");
       result["data"]=json_stringt(value_string);
     }
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
@@ -120,7 +120,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_array)
   {
-    auto sub = pointer_offset_bits(type.subtype(), ns);
+    auto sub = pointer_offset_bits(to_array_type(type).subtype(), ns);
     if(!sub.has_value())
       return {};
 
@@ -137,7 +137,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_vector)
   {
-    auto sub = pointer_offset_bits(type.subtype(), ns);
+    auto sub = pointer_offset_bits(to_vector_type(type).subtype(), ns);
     if(!sub.has_value())
       return {};
 
@@ -154,7 +154,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_complex)
   {
-    auto sub = pointer_offset_bits(type.subtype(), ns);
+    auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);
 
     if(sub.has_value())
       return (*sub) * 2;
@@ -212,7 +212,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_c_enum)
   {
-    return mp_integer(to_bitvector_type(type.subtype()).get_width());
+    return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -313,12 +313,14 @@ exprt size_of_expr(
 {
   if(type.id()==ID_array)
   {
-    exprt sub=size_of_expr(type.subtype(), ns);
+    const auto &array_type = to_array_type(type);
+
+    exprt sub = size_of_expr(array_type.subtype(), ns);
     if(sub.is_nil())
       return nil_exprt();
 
     // get size
-    exprt size=to_array_type(type).size();
+    exprt size = array_type.size();
 
     if(size.is_nil())
       return nil_exprt();
@@ -333,7 +335,7 @@ exprt size_of_expr(
   }
   else if(type.id()==ID_vector)
   {
-    exprt sub=size_of_expr(type.subtype(), ns);
+    exprt sub = size_of_expr(to_vector_type(type).subtype(), ns);
     if(sub.is_nil())
       return nil_exprt();
 
@@ -353,7 +355,7 @@ exprt size_of_expr(
   }
   else if(type.id()==ID_complex)
   {
-    exprt sub=size_of_expr(type.subtype(), ns);
+    exprt sub = size_of_expr(to_complex_type(type).subtype(), ns);
     if(sub.is_nil())
       return nil_exprt();
 
@@ -465,7 +467,8 @@ exprt size_of_expr(
   }
   else if(type.id()==ID_c_enum)
   {
-    std::size_t width=to_bitvector_type(type.subtype()).get_width();
+    std::size_t width =
+      to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
     std::size_t bytes=width/8;
     if(bytes*8!=width)
       bytes++;
@@ -529,15 +532,16 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)
   else if(expr.id()==ID_index)
   {
     const index_exprt &index_expr=to_index_expr(expr);
-    const typet &array_type=ns.follow(index_expr.array().type());
     DATA_INVARIANT(
-      array_type.id()==ID_array,
-      "index into array expected, found "+array_type.id_string());
+      index_expr.array().type().id() == ID_array,
+      "index into array expected, found " +
+        index_expr.array().type().id_string());
 
     auto o = compute_pointer_offset(index_expr.array(), ns);
 
     if(o.has_value())
     {
+      const auto &array_type = to_array_type(index_expr.array().type());
       auto sub_size = pointer_offset_size(array_type.subtype(), ns);
 
       mp_integer i;
diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
diff --git a/src/util/string_constant.cpp b/src/util/string_constant.cpp
diff --git a/src/util/xml_expr.cpp b/src/util/xml_expr.cpp

Original file line number	Diff line number	Diff line change
`@@ -616,8 +616,9 @@ void rw_range_sett::get_objects_rec(const typet &type)`
`616`	`616`	`// TODO should recurse into various composite types`
`617`	`617`	`if(type.id()==ID_array)`
`618`	`618`	`{`
`619`		`- get_objects_rec(type.subtype());`
`620`		`- get_objects_rec(get_modet::READ, to_array_type(type).size());`
	`619`	`+ const auto &array_type = to_array_type(type);`
	`620`	`+ get_objects_rec(array_type.subtype());`
	`621`	`+ get_objects_rec(get_modet::READ, array_type.size());`
`621`	`622`	`}`
`622`	`623`	`}`
`623`	`624`
Original file line number	Diff line number	Diff line change
`@@ -140,5 +140,7 @@ void mutex_init_instrumentation(goto_modelt &goto_model)`
`140`	`140`
`141`	`141`	`Forall_goto_functions(f_it, goto_model.goto_functions)`
`142`	`142`	`mutex_init_instrumentation(`
`143`		`- goto_model.symbol_table, f_it->second.body, lock_type.subtype());`
	`143`	`+ goto_model.symbol_table,`
	`144`	`+ f_it->second.body,`
	`145`	`+ to_pointer_type(lock_type).subtype());`
`144`	`146`	`}`
Original file line number	Diff line number	Diff line change
`@@ -211,7 +211,7 @@ static bool check_renaming(const typet &type)`
`211`	`211`	`return true;`
`212`	`212`	`}`
`213`	`213`	`else if(type.has_subtype())`
`214`		`- return check_renaming(type.subtype());`
	`214`	`+ return check_renaming(to_type_with_subtype(type).subtype());`
`215`	`215`
`216`	`216`	`return false;`
`217`	`217`	`}`
`@@ -489,7 +489,7 @@ void goto_symex_statet::rename(`
`489`	`489`	`{`
`490`	`490`	`auto &address_of_expr = to_address_of_expr(expr);`
`491`	`491`	`rename_address(address_of_expr.object(), ns, level);`
`492`		`- expr.type().subtype() = address_of_expr.object().type();`
	`492`	`+ to_pointer_type(expr.type()).subtype() = address_of_expr.object().type();`
`493`	`493`	`}`
`494`	`494`	`else`
`495`	`495`	`{`
`@@ -725,7 +725,7 @@ void goto_symex_statet::rename_address(`
`725`	`725`
`726`	`726`	`rename_address(index_expr.array(), ns, level);`
`727`	`727`	`PRECONDITION(index_expr.array().type().id() == ID_array);`
`728`		`- expr.type()=index_expr.array().type().subtype();`
	`728`	`+ expr.type() = to_array_type(index_expr.array().type()).subtype();`
`729`	`729`
`730`	`730`	`// the index is not an address`
`731`	`731`	`rename(index_expr.index(), ns, level);`
`@@ -810,8 +810,9 @@ void goto_symex_statet::rename(`
`810`	`810`
`811`	`811`	`if(type.id()==ID_array)`
`812`	`812`	`{`
`813`		`- rename(type.subtype(), irep_idt(), ns, level);`
`814`		`- rename(to_array_type(type).size(), ns, level);`
	`813`	`+ auto &array_type = to_array_type(type);`
	`814`	`+ rename(array_type.subtype(), irep_idt(), ns, level);`
	`815`	`+ rename(array_type.size(), ns, level);`
`815`	`816`	`}`
`816`	`817`	`else if(type.id()==ID_struct \|\|`
`817`	`818`	`type.id()==ID_union \|\|`
`@@ -832,7 +833,7 @@ void goto_symex_statet::rename(`
`832`	`833`	`}`
`833`	`834`	`else if(type.id()==ID_pointer)`
`834`	`835`	`{`
`835`		`- rename(type.subtype(), irep_idt(), ns, level);`
	`836`	`+ rename(to_pointer_type(type).subtype(), irep_idt(), ns, level);`
`836`	`837`	`}`
`837`	`838`	`else if(type.id() == ID_symbol_type)`
`838`	`839`	`{`
`@@ -876,8 +877,9 @@ void goto_symex_statet::get_original_name(typet &type) const`
`876`	`877`
`877`	`878`	`if(type.id()==ID_array)`
`878`	`879`	`{`
`879`		`- get_original_name(type.subtype());`
`880`		`- get_original_name(to_array_type(type).size());`
	`880`	`+ auto &array_type = to_array_type(type);`
	`881`	`+ get_original_name(array_type.subtype());`
	`882`	`+ get_original_name(array_type.size());`
`881`	`883`	`}`
`882`	`884`	`else if(type.id()==ID_struct \|\|`
`883`	`885`	`type.id()==ID_union \|\|`
`@@ -894,7 +896,7 @@ void goto_symex_statet::get_original_name(typet &type) const`
`894`	`896`	`}`
`895`	`897`	`else if(type.id()==ID_pointer)`
`896`	`898`	`{`
`897`		`- get_original_name(type.subtype());`
	`899`	`+ get_original_name(to_pointer_type(type).subtype());`
`898`	`900`	`}`
`899`	`901`	`}`
`900`	`902`
Original file line number	Diff line number	Diff line change
`@@ -60,9 +60,11 @@ void goto_symext::symex_allocate(`
`60`	`60`	`const irep_idt &mode = function_symbol->mode;`
`61`	`61`
`62`	`62`	`// is the type given?`
`63`		`- if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)`
	`63`	`+ if(`
	`64`	`+ code.type().id() == ID_pointer &&`
	`65`	`+ to_pointer_type(code.type()).subtype().id() != ID_empty)`
`64`	`66`	`{`
`65`		`- object_type=code.type().subtype();`
	`67`	`+ object_type = to_pointer_type(code.type()).subtype();`
`66`	`68`	`}`
`67`	`69`	`else`
`68`	`70`	`{`
`@@ -190,11 +192,11 @@ void goto_symext::symex_allocate(`
`190`	`192`
`191`	`193`	`if(object_type.id()==ID_array)`
`192`	`194`	`{`
`193`		`- index_exprt index_expr(value_symbol.type.subtype());`
	`195`	`+ const auto &array_type = to_array_type(object_type);`
	`196`	`+ index_exprt index_expr(array_type.subtype());`
`194`	`197`	`index_expr.array()=value_symbol.symbol_expr();`
`195`	`198`	`index_expr.index()=from_integer(0, index_type());`
`196`		`- rhs=address_of_exprt(`
`197`		`- index_expr, pointer_type(value_symbol.type.subtype()));`
	`199`	`+ rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));`
`198`	`200`	`}`
`199`	`201`	`else`
`200`	`202`	`{`
`@@ -391,6 +393,8 @@ void goto_symext::symex_cpp_new(`
`391`	`393`
`392`	`394`	`PRECONDITION(code.type().id() == ID_pointer);`
`393`	`395`
	`396`	`+ const auto &pointer_type = to_pointer_type(code.type());`
	`397`	`+`
`394`	`398`	`do_array =`
`395`	`399`	`(code.get(ID_statement) == ID_cpp_new_array \|\|`
`396`	`400`	`code.get(ID_statement) == ID_java_new_array_data);`
`@@ -418,19 +422,18 @@ void goto_symext::symex_cpp_new(`
`418`	`422`	`{`
`419`	`423`	`exprt size_arg = static_cast<const exprt &>(code.find(ID_size));`
`420`	`424`	`clean_expr(size_arg, state, false);`
`421`		`- symbol.type = array_typet(code.type().subtype(), size_arg);`
	`425`	`+ symbol.type = array_typet(pointer_type.subtype(), size_arg);`
`422`	`426`	`}`
`423`	`427`	`else`
`424`		`- symbol.type=code.type().subtype();`
	`428`	`+ symbol.type = pointer_type.subtype();`
`425`	`429`
`426`	`430`	`symbol.type.set(ID_C_dynamic, true);`
`427`	`431`
`428`	`432`	`state.symbol_table.add(symbol);`
`429`	`433`
`430`	`434`	`// make symbol expression`
`431`	`435`
`432`		`- exprt rhs(ID_address_of, code.type());`
`433`		`- rhs.type().subtype()=code.type().subtype();`
	`436`	`+ exprt rhs(ID_address_of, pointer_type);`
`434`	`437`
`435`	`438`	`if(do_array)`
`436`	`439`	`{`
Original file line number	Diff line number	Diff line change
`@@ -321,8 +321,11 @@ void goto_symext::dereference_rec(`
`321`	`321`	`exprt &object=address_of_expr.object();`
`322`	`322`
`323`	`323`	`const typet &expr_type=ns.follow(expr.type());`
`324`		`- expr=address_arithmetic(object, state, guard,`
`325`		`- expr_type.subtype().id()==ID_array);`
	`324`	`+ expr = address_arithmetic(`
	`325`	`+ object,`
	`326`	`+ state,`
	`327`	`+ guard,`
	`328`	`+ to_pointer_type(expr_type).subtype().id() == ID_array);`
`326`	`329`	`}`
`327`	`330`	`else if(expr.id()==ID_typecast)`
`328`	`331`	`{`
Original file line number	Diff line number	Diff line change
`@@ -72,7 +72,7 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`72`	`72`	`}`
`73`	`73`	`else if(type_id==ID_c_bit_field)`
`74`	`74`	`{`
`75`		`- const typet &subtype=type.subtype();`
	`75`	`+ const typet &subtype = to_c_bit_field_type(type).subtype();`
`76`	`76`	`if(subtype.id()==ID_signedbv)`
`77`	`77`	`{`
`78`	`78`	`int_value=binary2integer(id2string(value), true);`
Original file line number	Diff line number	Diff line change
`@@ -116,7 +116,8 @@ exprt expr_initializert<nondet>::expr_initializer_rec(`
`116`	`116`	`result = side_effect_expr_nondett(type, source_location);`
`117`	`117`	`else`
`118`	`118`	`{`
`119`		`- exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);`
	`119`	`+ exprt sub_zero =`
	`120`	`+ expr_initializer_rec(to_complex_type(type).subtype(), source_location);`
`120`	`121`	`result = complex_exprt(sub_zero, sub_zero, to_complex_type(type));`
`121`	`122`	`}`
`122`	`123`
Original file line number	Diff line number	Diff line change
`@@ -124,7 +124,7 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)`
`124`	`124`	`src.id()!=ID_pointer)`
`125`	`125`	`{`
`126`	`126`	`if(src.has_subtype())`
`127`		`- find_symbols(kind, src.subtype(), dest);`
	`127`	`+ find_symbols(kind, to_type_with_subtype(src).subtype(), dest);`
`128`	`128`
`129`	`129`	`forall_subtypes(it, src)`
`130`	`130`	`find_symbols(kind, *it, dest);`
Original file line number	Diff line number	Diff line change
`@@ -154,7 +154,10 @@ json_objectt json(`
`154`	`154`	`else if(type.id()==ID_c_enum_tag)`
`155`	`155`	`{`
`156`	`156`	`// we return the base type`
`157`		`- return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);`
	`157`	`+ return json(`
	`158`	`+ to_c_enum_type(ns.follow_tag(to_c_enum_tag_type(type))).subtype(),`
	`159`	`+ ns,`
	`160`	`+ mode);`
`158`	`161`	`}`
`159`	`162`	`else if(type.id()==ID_fixedbv)`
`160`	`163`	`{`
`@@ -165,7 +168,7 @@ json_objectt json(`
`165`	`168`	`else if(type.id()==ID_pointer)`
`166`	`169`	`{`
`167`	`170`	`result["name"]=json_stringt("pointer");`
`168`		`- result["subtype"]=json(type.subtype(), ns, mode);`
	`171`	`+ result["subtype"] = json(to_pointer_type(type).subtype(), ns, mode);`
`169`	`172`	`}`
`170`	`173`	`else if(type.id()==ID_bool)`
`171`	`174`	`{`
`@@ -174,12 +177,12 @@ json_objectt json(`
`174`	`177`	`else if(type.id()==ID_array)`
`175`	`178`	`{`
`176`	`179`	`result["name"]=json_stringt("array");`
`177`		`- result["subtype"]=json(type.subtype(), ns, mode);`
	`180`	`+ result["subtype"] = json(to_array_type(type).subtype(), ns, mode);`
`178`	`181`	`}`
`179`	`182`	`else if(type.id()==ID_vector)`
`180`	`183`	`{`
`181`	`184`	`result["name"]=json_stringt("vector");`
`182`		`- result["subtype"]=json(type.subtype(), ns, mode);`
	`185`	`+ result["subtype"] = json(to_vector_type(type).subtype(), ns, mode);`
`183`	`186`	`result["size"]=json(to_vector_type(type).size(), ns, mode);`
`184`	`187`	`}`
`185`	`188`	`else if(type.id()==ID_struct)`
`@@ -242,9 +245,8 @@ json_objectt json(`
`242`	`245`	`lang=std::unique_ptr<languaget>(get_default_language());`
`243`	`246`	`}`
`244`	`247`
`245`		`- const typet &underlying_type=`
`246`		`- type.id()==ID_c_bit_field?type.subtype():`
`247`		`- type;`
	`248`	`+ const typet &underlying_type =`
	`249`	`+ type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;`
`248`	`250`
`249`	`251`	`std::string type_string;`
`250`	`252`	`bool error=lang->from_type(underlying_type, type_string, ns);`
`@@ -270,7 +272,8 @@ json_objectt json(`
`270`	`272`	`{`
`271`	`273`	`result["name"]=json_stringt("integer");`
`272`	`274`	`result["binary"] = json_stringt(constant_expr.get_value());`
`273`		`- result["width"]=json_numbert(type.subtype().get_string(ID_width));`
	`275`	`+ result["width"] =`
	`276`	`+ json_numbert(to_c_enum_type(type).subtype().get_string(ID_width));`
`274`	`277`	`result["type"]=json_stringt("enum");`
`275`	`278`	`result["data"]=json_stringt(value_string);`
`276`	`279`	`}`
Original file line number	Diff line number	Diff line change
`@@ -120,7 +120,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)`
`120`	`120`	`{`
`121`	`121`	`if(type.id()==ID_array)`
`122`	`122`	`{`
`123`		`- auto sub = pointer_offset_bits(type.subtype(), ns);`
	`123`	`+ auto sub = pointer_offset_bits(to_array_type(type).subtype(), ns);`
`124`	`124`	`if(!sub.has_value())`
`125`	`125`	`return {};`
`126`	`126`
`@@ -137,7 +137,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)`
`137`	`137`	`}`
`138`	`138`	`else if(type.id()==ID_vector)`
`139`	`139`	`{`
`140`		`- auto sub = pointer_offset_bits(type.subtype(), ns);`
	`140`	`+ auto sub = pointer_offset_bits(to_vector_type(type).subtype(), ns);`
`141`	`141`	`if(!sub.has_value())`
`142`	`142`	`return {};`
`143`	`143`
`@@ -154,7 +154,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)`
`154`	`154`	`}`
`155`	`155`	`else if(type.id()==ID_complex)`
`156`	`156`	`{`
`157`		`- auto sub = pointer_offset_bits(type.subtype(), ns);`
	`157`	`+ auto sub = pointer_offset_bits(to_complex_type(type).subtype(), ns);`
`158`	`158`
`159`	`159`	`if(sub.has_value())`
`160`	`160`	`return (sub) 2;`
`@@ -212,7 +212,7 @@ pointer_offset_bits(const typet &type, const namespacet &ns)`
`212`	`212`	`}`
`213`	`213`	`else if(type.id()==ID_c_enum)`
`214`	`214`	`{`
`215`		`- return mp_integer(to_bitvector_type(type.subtype()).get_width());`
	`215`	`+ return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());`
`216`	`216`	`}`
`217`	`217`	`else if(type.id()==ID_c_enum_tag)`
`218`	`218`	`{`
`@@ -313,12 +313,14 @@ exprt size_of_expr(`
`313`	`313`	`{`
`314`	`314`	`if(type.id()==ID_array)`
`315`	`315`	`{`
`316`		`- exprt sub=size_of_expr(type.subtype(), ns);`
	`316`	`+ const auto &array_type = to_array_type(type);`
	`317`	`+`
	`318`	`+ exprt sub = size_of_expr(array_type.subtype(), ns);`
`317`	`319`	`if(sub.is_nil())`
`318`	`320`	`return nil_exprt();`
`319`	`321`
`320`	`322`	`// get size`
`321`		`- exprt size=to_array_type(type).size();`
	`323`	`+ exprt size = array_type.size();`
`322`	`324`
`323`	`325`	`if(size.is_nil())`
`324`	`326`	`return nil_exprt();`
`@@ -333,7 +335,7 @@ exprt size_of_expr(`
`333`	`335`	`}`
`334`	`336`	`else if(type.id()==ID_vector)`
`335`	`337`	`{`
`336`		`- exprt sub=size_of_expr(type.subtype(), ns);`
	`338`	`+ exprt sub = size_of_expr(to_vector_type(type).subtype(), ns);`
`337`	`339`	`if(sub.is_nil())`
`338`	`340`	`return nil_exprt();`
`339`	`341`
`@@ -353,7 +355,7 @@ exprt size_of_expr(`
`353`	`355`	`}`
`354`	`356`	`else if(type.id()==ID_complex)`
`355`	`357`	`{`
`356`		`- exprt sub=size_of_expr(type.subtype(), ns);`
	`358`	`+ exprt sub = size_of_expr(to_complex_type(type).subtype(), ns);`
`357`	`359`	`if(sub.is_nil())`
`358`	`360`	`return nil_exprt();`
`359`	`361`
`@@ -465,7 +467,8 @@ exprt size_of_expr(`
`465`	`467`	`}`
`466`	`468`	`else if(type.id()==ID_c_enum)`
`467`	`469`	`{`
`468`		`- std::size_t width=to_bitvector_type(type.subtype()).get_width();`
	`470`	`+ std::size_t width =`
	`471`	`+ to_bitvector_type(to_c_enum_type(type).subtype()).get_width();`
`469`	`472`	`std::size_t bytes=width/8;`
`470`	`473`	`if(bytes*8!=width)`
`471`	`474`	`bytes++;`
`@@ -529,15 +532,16 @@ compute_pointer_offset(const exprt &expr, const namespacet &ns)`
`529`	`532`	`else if(expr.id()==ID_index)`
`530`	`533`	`{`
`531`	`534`	`const index_exprt &index_expr=to_index_expr(expr);`
`532`		`- const typet &array_type=ns.follow(index_expr.array().type());`
`533`	`535`	`DATA_INVARIANT(`
`534`		`- array_type.id()==ID_array,`
`535`		`- "index into array expected, found "+array_type.id_string());`
	`536`	`+ index_expr.array().type().id() == ID_array,`
	`537`	`+ "index into array expected, found " +`
	`538`	`+ index_expr.array().type().id_string());`
`536`	`539`
`537`	`540`	`auto o = compute_pointer_offset(index_expr.array(), ns);`
`538`	`541`
`539`	`542`	`if(o.has_value())`
`540`	`543`	`{`
	`544`	`+ const auto &array_type = to_array_type(index_expr.array().type());`
`541`	`545`	`auto sub_size = pointer_offset_size(array_type.subtype(), ns);`
`542`	`546`
`543`	`547`	`mp_integer i;`