Do not hardcode char/bytes having 8 bits

tautschnig · tautschnig · commit 2b06c7b29fd7 · 2021-04-03T21:50:49.000Z
The C standard does not guarantee that char is exactly 8 bits, and there are
DSPs (such Texas Instruments C55x) that do not have 8-bit-bytes. Use the
configuration value instead.
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
@@ -22,8 +22,8 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, to
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (183), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'c_types.h' not generated, too many nodes (143), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'c_types.h' not generated, too many nodes (144), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/ansi-c/literals/convert_character_literal.cpp b/src/ansi-c/literals/convert_character_literal.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/std_expr.h>
 
 #include "unescape_string.h"
@@ -51,7 +52,7 @@ exprt convert_character_literal(
       for(unsigned i=0; i<value.size(); i++)
       {
         mp_integer z=(unsigned char)(value[i]);
-        z=z<<((value.size()-i-1)*8);
+        z = z << ((value.size() - i - 1) * config.ansi_c.char_width);
         x+=z;
       }
 
@@ -84,7 +85,7 @@ exprt convert_character_literal(
       for(unsigned i=0; i<value.size(); i++)
       {
         mp_integer z=(unsigned char)(value[i]);
-        z=z<<((value.size()-i-1)*8);
+        z = z << ((value.size() - i - 1) * config.ansi_c.char_width);
         x+=z;
       }
 
diff --git a/src/goto-instrument/stack_depth.cpp b/src/goto-instrument/stack_depth.cpp
@@ -15,6 +15,7 @@ Date: November 2011
 
 #include <util/arith_tools.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -23,7 +24,7 @@ Date: November 2011
 symbol_exprt add_stack_depth_symbol(symbol_tablet &symbol_table)
 {
   const irep_idt identifier="$stack_depth";
-  unsignedbv_typet type(sizeof(std::size_t)*8);
+  typet type = size_type();
 
   symbolt new_symbol;
   new_symbol.name=identifier;
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
@@ -38,14 +38,14 @@ optionalt<mp_integer> member_offset(
     {
       const std::size_t w = to_c_bit_field_type(comp.type()).get_width();
       bit_field_bits += w;
-      result += bit_field_bits / 8;
-      bit_field_bits %= 8;
+      result += bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
     }
     else if(comp.type().id() == ID_bool)
     {
       ++bit_field_bits;
-      result += bit_field_bits / 8;
-      bit_field_bits %= 8;
+      result += bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
     }
     else
     {
@@ -92,7 +92,7 @@ pointer_offset_size(const typet &type, const namespacet &ns)
   auto bits = pointer_offset_bits(type, ns);
 
   if(bits.has_value())
-    return (*bits + 7) / 8;
+    return (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
   else
     return {};
 }
@@ -248,16 +248,16 @@ optionalt<exprt> member_offset_expr(
     {
       std::size_t w = to_c_bit_field_type(c.type()).get_width();
       bit_field_bits += w;
-      const std::size_t bytes = bit_field_bits / 8;
-      bit_field_bits %= 8;
+      const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
       if(bytes > 0)
         result = plus_exprt(result, from_integer(bytes, result.type()));
     }
     else if(c.type().id() == ID_bool)
     {
       ++bit_field_bits;
-      const std::size_t bytes = bit_field_bits / 8;
-      bit_field_bits %= 8;
+      const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+      bit_field_bits %= config.ansi_c.char_width;
       if(bytes > 0)
         result = plus_exprt(result, from_integer(bytes, result.type()));
     }
@@ -288,7 +288,9 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       auto bits = pointer_offset_bits(array_type, ns);
 
       if(bits.has_value())
-        return from_integer((*bits + 7) / 8, size_type());
+        return from_integer(
+          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
+          size_type());
     }
 
     auto sub = size_of_expr(array_type.subtype(), ns);
@@ -315,7 +317,9 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       auto bits = pointer_offset_bits(vector_type, ns);
 
       if(bits.has_value())
-        return from_integer((*bits + 7) / 8, size_type());
+        return from_integer(
+          (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,
+          size_type());
     }
 
     auto sub = size_of_expr(vector_type.subtype(), ns);
@@ -354,16 +358,16 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       {
         std::size_t w = to_c_bit_field_type(c.type()).get_width();
         bit_field_bits += w;
-        const std::size_t bytes = bit_field_bits / 8;
-        bit_field_bits %= 8;
+        const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+        bit_field_bits %= config.ansi_c.char_width;
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
       else if(c.type().id() == ID_bool)
       {
         ++bit_field_bits;
-        const std::size_t bytes = bit_field_bits / 8;
-        bit_field_bits %= 8;
+        const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;
+        bit_field_bits %= config.ansi_c.char_width;
         if(bytes > 0)
           result = plus_exprt(result, from_integer(bytes, result.type()));
       }
@@ -409,7 +413,8 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
       }
       else
       {
-        mp_integer sub_bytes = (*sub_bits + 7) / 8;
+        mp_integer sub_bytes =
+          (*sub_bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
 
         if(max_bytes>=0)
         {
@@ -443,19 +448,14 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
           type.id()==ID_c_bit_field)
   {
     std::size_t width=to_bitvector_type(type).get_width();
-    std::size_t bytes=width/8;
-    if(bytes*8!=width)
+    std::size_t bytes = width / config.ansi_c.char_width;
+    if(bytes * config.ansi_c.char_width != width)
       bytes++;
     return from_integer(bytes, size_type());
   }
   else if(type.id()==ID_c_enum)
   {
-    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++;
-    return from_integer(bytes, size_type());
+    return size_of_expr(to_c_enum_type(type).subtype(), ns);
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -469,11 +469,11 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
   {
     // the following is an MS extension
     if(type.get_bool(ID_C_ptr32))
-      return from_integer(4, size_type());
+      return from_integer(32 / config.ansi_c.char_width, size_type());
 
     std::size_t width=to_bitvector_type(type).get_width();
-    std::size_t bytes=width/8;
-    if(bytes*8!=width)
+    std::size_t bytes = width / config.ansi_c.char_width;
+    if(bytes * config.ansi_c.char_width != width)
       bytes++;
     return from_integer(bytes, size_type());
   }
@@ -491,7 +491,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_string)
   {
-    return from_integer(32/8, size_type());
+    return from_integer(32 / config.ansi_c.char_width, size_type());
   }
   else
     return {};
@@ -645,12 +645,17 @@ optionalt<exprt> get_subexpression_at_offset(
       // if this member completely contains the target, and this member is
       // byte-aligned, recurse into it
       if(
-        offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
-        offset_bytes * 8 + *target_size_bits <= m_offset_bits + *m_size_bits)
+        offset_bytes * config.ansi_c.char_width >= m_offset_bits &&
+        m_offset_bits % config.ansi_c.char_width == 0 &&
+        offset_bytes * config.ansi_c.char_width + *target_size_bits <=
+          m_offset_bits + *m_size_bits)
       {
         const member_exprt member(expr, component.get_name(), component.type());
         return get_subexpression_at_offset(
-          member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);
+          member,
+          offset_bytes - m_offset_bits / config.ansi_c.char_width,
+          target_type_raw,
+          ns);
       }
 
       m_offset_bits += *m_size_bits;
@@ -665,11 +670,14 @@ optionalt<exprt> get_subexpression_at_offset(
     // no arrays of non-byte-aligned, zero-, or unknown-sized objects
     if(
       elem_size_bits.has_value() && *elem_size_bits > 0 &&
-      *elem_size_bits % 8 == 0 && *target_size_bits <= *elem_size_bits)
+      *elem_size_bits % config.ansi_c.char_width == 0 &&
+      *target_size_bits <= *elem_size_bits)
     {
-      const mp_integer elem_size_bytes = *elem_size_bits / 8;
+      const mp_integer elem_size_bytes =
+        *elem_size_bits / config.ansi_c.char_width;
       const auto offset_inside_elem = offset_bytes % elem_size_bytes;
-      const auto target_size_bytes = *target_size_bits / 8;
+      const auto target_size_bytes =
+        *target_size_bits / config.ansi_c.char_width;
       // only recurse if the cell completely contains the target
       if(offset_inside_elem + target_size_bytes <= elem_size_bytes)
       {
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
@@ -774,6 +774,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   }
 
   // circular casts through types shorter than `int`
+  // we use fixed bit widths as this is specifically for the Java bytecode
+  // front-end
   if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)
   {
     if(expr_type==c_bool_typet(8) ||
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
+#include "config.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
@@ -194,7 +195,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
 
     if(target_size.has_value())
     {
-      mp_integer target_bits = target_size.value() * 8;
+      mp_integer target_bits = target_size.value() * config.ansi_c.char_width;
       const auto bits = expr2bits(op, true, ns);
 
       if(bits.has_value() &&

Original file line number	Diff line number	Diff line change
`@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]`
`13`	`13`
`14`	`14`	`#include <util/arith_tools.h>`
`15`	`15`	`#include <util/c_types.h>`
	`16`	`+#include <util/config.h>`
`16`	`17`	`#include <util/std_expr.h>`
`17`	`18`
`18`	`19`	`#include "unescape_string.h"`
`@@ -51,7 +52,7 @@ exprt convert_character_literal(`
`51`	`52`	`for(unsigned i=0; i<value.size(); i++)`
`52`	`53`	`{`
`53`	`54`	`mp_integer z=(unsigned char)(value[i]);`
`54`		`- z=z<<((value.size()-i-1)*8);`
	`55`	`+ z = z << ((value.size() - i - 1) * config.ansi_c.char_width);`
`55`	`56`	`x+=z;`
`56`	`57`	`}`
`57`	`58`
`@@ -84,7 +85,7 @@ exprt convert_character_literal(`
`84`	`85`	`for(unsigned i=0; i<value.size(); i++)`
`85`	`86`	`{`
`86`	`87`	`mp_integer z=(unsigned char)(value[i]);`
`87`		`- z=z<<((value.size()-i-1)*8);`
	`88`	`+ z = z << ((value.size() - i - 1) * config.ansi_c.char_width);`
`88`	`89`	`x+=z;`
`89`	`90`	`}`
`90`	`91`
Original file line number	Diff line number	Diff line change
`@@ -38,14 +38,14 @@ optionalt<mp_integer> member_offset(`
`38`	`38`	`{`
`39`	`39`	`const std::size_t w = to_c_bit_field_type(comp.type()).get_width();`
`40`	`40`	`bit_field_bits += w;`
`41`		`- result += bit_field_bits / 8;`
`42`		`- bit_field_bits %= 8;`
	`41`	`+ result += bit_field_bits / config.ansi_c.char_width;`
	`42`	`+ bit_field_bits %= config.ansi_c.char_width;`
`43`	`43`	`}`
`44`	`44`	`else if(comp.type().id() == ID_bool)`
`45`	`45`	`{`
`46`	`46`	`++bit_field_bits;`
`47`		`- result += bit_field_bits / 8;`
`48`		`- bit_field_bits %= 8;`
	`47`	`+ result += bit_field_bits / config.ansi_c.char_width;`
	`48`	`+ bit_field_bits %= config.ansi_c.char_width;`
`49`	`49`	`}`
`50`	`50`	`else`
`51`	`51`	`{`
`@@ -92,7 +92,7 @@ pointer_offset_size(const typet &type, const namespacet &ns)`
`92`	`92`	`auto bits = pointer_offset_bits(type, ns);`
`93`	`93`
`94`	`94`	`if(bits.has_value())`
`95`		`- return (*bits + 7) / 8;`
	`95`	`+ return (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;`
`96`	`96`	`else`
`97`	`97`	`return {};`
`98`	`98`	`}`
`@@ -248,16 +248,16 @@ optionalt<exprt> member_offset_expr(`
`248`	`248`	`{`
`249`	`249`	`std::size_t w = to_c_bit_field_type(c.type()).get_width();`
`250`	`250`	`bit_field_bits += w;`
`251`		`- const std::size_t bytes = bit_field_bits / 8;`
`252`		`- bit_field_bits %= 8;`
	`251`	`+ const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;`
	`252`	`+ bit_field_bits %= config.ansi_c.char_width;`
`253`	`253`	`if(bytes > 0)`
`254`	`254`	`result = plus_exprt(result, from_integer(bytes, result.type()));`
`255`	`255`	`}`
`256`	`256`	`else if(c.type().id() == ID_bool)`
`257`	`257`	`{`
`258`	`258`	`++bit_field_bits;`
`259`		`- const std::size_t bytes = bit_field_bits / 8;`
`260`		`- bit_field_bits %= 8;`
	`259`	`+ const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;`
	`260`	`+ bit_field_bits %= config.ansi_c.char_width;`
`261`	`261`	`if(bytes > 0)`
`262`	`262`	`result = plus_exprt(result, from_integer(bytes, result.type()));`
`263`	`263`	`}`
`@@ -288,7 +288,9 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`288`	`288`	`auto bits = pointer_offset_bits(array_type, ns);`
`289`	`289`
`290`	`290`	`if(bits.has_value())`
`291`		`- return from_integer((*bits + 7) / 8, size_type());`
	`291`	`+ return from_integer(`
	`292`	`+ (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,`
	`293`	`+ size_type());`
`292`	`294`	`}`
`293`	`295`
`294`	`296`	`auto sub = size_of_expr(array_type.subtype(), ns);`
`@@ -315,7 +317,9 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`315`	`317`	`auto bits = pointer_offset_bits(vector_type, ns);`
`316`	`318`
`317`	`319`	`if(bits.has_value())`
`318`		`- return from_integer((*bits + 7) / 8, size_type());`
	`320`	`+ return from_integer(`
	`321`	`+ (*bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width,`
	`322`	`+ size_type());`
`319`	`323`	`}`
`320`	`324`
`321`	`325`	`auto sub = size_of_expr(vector_type.subtype(), ns);`
`@@ -354,16 +358,16 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`354`	`358`	`{`
`355`	`359`	`std::size_t w = to_c_bit_field_type(c.type()).get_width();`
`356`	`360`	`bit_field_bits += w;`
`357`		`- const std::size_t bytes = bit_field_bits / 8;`
`358`		`- bit_field_bits %= 8;`
	`361`	`+ const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;`
	`362`	`+ bit_field_bits %= config.ansi_c.char_width;`
`359`	`363`	`if(bytes > 0)`
`360`	`364`	`result = plus_exprt(result, from_integer(bytes, result.type()));`
`361`	`365`	`}`
`362`	`366`	`else if(c.type().id() == ID_bool)`
`363`	`367`	`{`
`364`	`368`	`++bit_field_bits;`
`365`		`- const std::size_t bytes = bit_field_bits / 8;`
`366`		`- bit_field_bits %= 8;`
	`369`	`+ const std::size_t bytes = bit_field_bits / config.ansi_c.char_width;`
	`370`	`+ bit_field_bits %= config.ansi_c.char_width;`
`367`	`371`	`if(bytes > 0)`
`368`	`372`	`result = plus_exprt(result, from_integer(bytes, result.type()));`
`369`	`373`	`}`
`@@ -409,7 +413,8 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`409`	`413`	`}`
`410`	`414`	`else`
`411`	`415`	`{`
`412`		`- mp_integer sub_bytes = (*sub_bits + 7) / 8;`
	`416`	`+ mp_integer sub_bytes =`
	`417`	`+ (*sub_bits + config.ansi_c.char_width - 1) / config.ansi_c.char_width;`
`413`	`418`
`414`	`419`	`if(max_bytes>=0)`
`415`	`420`	`{`
`@@ -443,19 +448,14 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`443`	`448`	`type.id()==ID_c_bit_field)`
`444`	`449`	`{`
`445`	`450`	`std::size_t width=to_bitvector_type(type).get_width();`
`446`		`- std::size_t bytes=width/8;`
`447`		`- if(bytes*8!=width)`
	`451`	`+ std::size_t bytes = width / config.ansi_c.char_width;`
	`452`	`+ if(bytes * config.ansi_c.char_width != width)`
`448`	`453`	`bytes++;`
`449`	`454`	`return from_integer(bytes, size_type());`
`450`	`455`	`}`
`451`	`456`	`else if(type.id()==ID_c_enum)`
`452`	`457`	`{`
`453`		`- std::size_t width =`
`454`		`- to_bitvector_type(to_c_enum_type(type).subtype()).get_width();`
`455`		`- std::size_t bytes=width/8;`
`456`		`- if(bytes*8!=width)`
`457`		`- bytes++;`
`458`		`- return from_integer(bytes, size_type());`
	`458`	`+ return size_of_expr(to_c_enum_type(type).subtype(), ns);`
`459`	`459`	`}`
`460`	`460`	`else if(type.id()==ID_c_enum_tag)`
`461`	`461`	`{`
`@@ -469,11 +469,11 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`469`	`469`	`{`
`470`	`470`	`// the following is an MS extension`
`471`	`471`	`if(type.get_bool(ID_C_ptr32))`
`472`		`- return from_integer(4, size_type());`
	`472`	`+ return from_integer(32 / config.ansi_c.char_width, size_type());`
`473`	`473`
`474`	`474`	`std::size_t width=to_bitvector_type(type).get_width();`
`475`		`- std::size_t bytes=width/8;`
`476`		`- if(bytes*8!=width)`
	`475`	`+ std::size_t bytes = width / config.ansi_c.char_width;`
	`476`	`+ if(bytes * config.ansi_c.char_width != width)`
`477`	`477`	`bytes++;`
`478`	`478`	`return from_integer(bytes, size_type());`
`479`	`479`	`}`
`@@ -491,7 +491,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)`
`491`	`491`	`}`
`492`	`492`	`else if(type.id()==ID_string)`
`493`	`493`	`{`
`494`		`- return from_integer(32/8, size_type());`
	`494`	`+ return from_integer(32 / config.ansi_c.char_width, size_type());`
`495`	`495`	`}`
`496`	`496`	`else`
`497`	`497`	`return {};`
`@@ -645,12 +645,17 @@ optionalt<exprt> get_subexpression_at_offset(`
`645`	`645`	`// if this member completely contains the target, and this member is`
`646`	`646`	`// byte-aligned, recurse into it`
`647`	`647`	`if(`
`648`		`- offset_bytes * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&`
`649`		`- offset_bytes * 8 + target_size_bits <= m_offset_bits + m_size_bits)`
	`648`	`+ offset_bytes * config.ansi_c.char_width >= m_offset_bits &&`
	`649`	`+ m_offset_bits % config.ansi_c.char_width == 0 &&`
	`650`	`+ offset_bytes * config.ansi_c.char_width + *target_size_bits <=`
	`651`	`+ m_offset_bits + *m_size_bits)`
`650`	`652`	`{`
`651`	`653`	`const member_exprt member(expr, component.get_name(), component.type());`
`652`	`654`	`return get_subexpression_at_offset(`
`653`		`- member, offset_bytes - m_offset_bits / 8, target_type_raw, ns);`
	`655`	`+ member,`
	`656`	`+ offset_bytes - m_offset_bits / config.ansi_c.char_width,`
	`657`	`+ target_type_raw,`
	`658`	`+ ns);`
`654`	`659`	`}`
`655`	`660`
`656`	`661`	`m_offset_bits += *m_size_bits;`
`@@ -665,11 +670,14 @@ optionalt<exprt> get_subexpression_at_offset(`
`665`	`670`	`// no arrays of non-byte-aligned, zero-, or unknown-sized objects`
`666`	`671`	`if(`
`667`	`672`	`elem_size_bits.has_value() && *elem_size_bits > 0 &&`
`668`		`- elem_size_bits % 8 == 0 && target_size_bits <= *elem_size_bits)`
	`673`	`+ *elem_size_bits % config.ansi_c.char_width == 0 &&`
	`674`	`+ target_size_bits <= elem_size_bits)`
`669`	`675`	`{`
`670`		`- const mp_integer elem_size_bytes = *elem_size_bits / 8;`
	`676`	`+ const mp_integer elem_size_bytes =`
	`677`	`+ *elem_size_bits / config.ansi_c.char_width;`
`671`	`678`	`const auto offset_inside_elem = offset_bytes % elem_size_bytes;`
`672`		`- const auto target_size_bytes = *target_size_bits / 8;`
	`679`	`+ const auto target_size_bytes =`
	`680`	`+ *target_size_bits / config.ansi_c.char_width;`
`673`	`681`	`// only recurse if the cell completely contains the target`
`674`	`682`	`if(offset_inside_elem + target_size_bytes <= elem_size_bytes)`
`675`	`683`	`{`
Original file line number	Diff line number	Diff line change
`@@ -774,6 +774,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)`
`774`	`774`	`}`
`775`	`775`
`776`	`776`	// circular casts through types shorter than `int`
	`777`	`+ // we use fixed bit widths as this is specifically for the Java bytecode`
	`778`	`+ // front-end`
`777`	`779`	`if(op_type == signedbv_typet(32) && expr.op().id() == ID_typecast)`
`778`	`780`	`{`
`779`	`781`	`if(expr_type==c_bool_typet(8) \|\|`