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()
24
24
return ID_byte_extract_big_endian;
25
25
26
26
case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
27
- UNREACHABLE ;
27
+ break ;
28
28
}
29
+
30
+ UNREACHABLE;
31
+ return ID_nil;
29
32
}
30
33
31
34
irep_idt byte_update_id ()
@@ -39,6 +42,9 @@ irep_idt byte_update_id()
39
42
return ID_byte_update_big_endian;
40
43
41
44
case configt::ansi_ct::endiannesst::NO_ENDIANNESS:
42
- UNREACHABLE ;
45
+ break ;
43
46
}
47
+
48
+ UNREACHABLE;
49
+ return ID_nil;
44
50
}
Original file line number Diff line number Diff line change @@ -68,7 +68,10 @@ unsignedbv_typet size_type()
68
68
else if (config.ansi_c .pointer_width ==config.ansi_c .long_long_int_width )
69
69
return unsigned_long_long_int_type ();
70
70
else
71
+ {
71
72
INVARIANT (false , " width of size type" ); // aaah!
73
+ return unsignedbv_typet (0 );
74
+ }
72
75
}
73
76
74
77
signedbv_typet signed_size_type ()
@@ -237,7 +240,10 @@ signedbv_typet pointer_diff_type()
237
240
else if (config.ansi_c .pointer_width ==config.ansi_c .long_long_int_width )
238
241
return signed_long_long_int_type ();
239
242
else
243
+ {
240
244
INVARIANT (false , " width of pointer difference" );
245
+ return signedbv_typet (0 );
246
+ }
241
247
}
242
248
243
249
pointer_typet pointer_type (const typet &subtype)
You can’t perform that action at this time.
0 commit comments