Use pointer_offset_bits instead of locally hacking up what it does anyway

Author: tautschnig

src/goto-programs/vcd_goto_trace.cpp

@@ -63,17 +63,7 @@ std::string as_vcd_binary(
 
   // build "xxx"
 
-  mp_integer width;
-
-  if(type.id()==ID_unsignedbv ||
-     type.id()==ID_signedbv ||
-     type.id()==ID_floatbv ||
-     type.id()==ID_fixedbv ||
-     type.id()==ID_pointer ||
-     type.id()==ID_bv)
-    width=string2integer(type.get_string(ID_width));
-  else
-    width=pointer_offset_size(type, ns)*8;
+  const mp_integer width = pointer_offset_bits(type, ns);
 
   if(width>=0)
     return std::string(integer2size_t(width), 'x');
@@ -106,12 +96,7 @@ void output_vcd(
 
       const auto number=n.number(identifier);
 
-      mp_integer width;
-
-      if(type.id()==ID_bool)
-        width=1;
-      else
-        width=pointer_offset_bits(type, ns);
+      const mp_integer width = pointer_offset_bits(type, ns);
 
       if(width>=1)
         out << "$var reg " << width << " V" << number << " "

src/pointer-analysis/value_set_dereference.cpp

@@ -712,20 +712,6 @@ void value_set_dereferencet::bounds_check(
   }
 }
 
-inline static unsigned bv_width(
-  const typet &type,
-  const namespacet &ns)
-{
-  if(type.id()==ID_c_enum_tag)
-  {
-    const typet &t=ns.follow_tag(to_c_enum_tag_type(type));
-    assert(t.id()==ID_c_enum);
-    return bv_width(t.subtype(), ns);
-  }
-
-  return unsafe_string2unsigned(type.get_string(ID_width));
-}
-
 static bool is_a_bv_type(const typet &type)
 {
   return type.id()==ID_unsignedbv ||
@@ -752,7 +738,7 @@ bool value_set_dereferencet::memory_model(
   if(is_a_bv_type(from_type) &&
      is_a_bv_type(to_type))
   {
-    if(bv_width(from_type, ns)==bv_width(to_type, ns))
+    if(pointer_offset_bits(from_type, ns) == pointer_offset_bits(to_type, ns))
     {
       // avoid semantic conversion in case of
       // cast to float or fixed-point,
@@ -772,7 +758,7 @@ bool value_set_dereferencet::memory_model(
   if(from_type.id()==ID_pointer &&
      to_type.id()==ID_pointer)
   {
-    if(bv_width(from_type, ns)==bv_width(to_type, ns))
+    if(pointer_offset_bits(from_type, ns) == pointer_offset_bits(to_type, ns))
       return memory_model_conversion(value, to_type, guard, offset);
   }