File tree Expand file tree Collapse file tree 2 files changed +14
-2
lines changed
Expand file tree Collapse file tree 2 files changed +14
-2
lines changed Original file line number Diff line number Diff line change @@ -24,8 +24,11 @@ irep_idt byte_extract_id()
2424 return ID_byte_extract_big_endian;
2525
2626 case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
27- UNREACHABLE ;
27+ break ;
2828 }
29+
30+ UNREACHABLE;
31+ return ID_nil;
2932}
3033
3134irep_idt byte_update_id ()
@@ -39,6 +42,9 @@ irep_idt byte_update_id()
3942 return ID_byte_update_big_endian;
4043
4144 case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
42- UNREACHABLE ;
45+ break ;
4346 }
47+
48+ UNREACHABLE;
49+ return ID_nil;
4450}
Original file line number Diff line number Diff line change @@ -68,7 +68,10 @@ unsignedbv_typet size_type()
6868 else if (config.ansi_c .pointer_width ==config.ansi_c .long_long_int_width )
6969 return unsigned_long_long_int_type ();
7070 else
71+ {
7172 INVARIANT (false , " width of size type" ); // aaah!
73+ return unsignedbv_typet (0 );
74+ }
7275}
7376
7477signedbv_typet signed_size_type ()
@@ -237,7 +240,10 @@ signedbv_typet pointer_diff_type()
237240 else if (config.ansi_c .pointer_width ==config.ansi_c .long_long_int_width )
238241 return signed_long_long_int_type ();
239242 else
243+ {
240244 INVARIANT (false , " width of pointer difference" );
245+ return signedbv_typet (0 );
246+ }
241247}
242248
243249pointer_typet pointer_type (const typet &subtype)
You can’t perform that action at this time.
0 commit comments