File tree 1 file changed +11
-13
lines changed
1 file changed +11
-13
lines changed Original file line number Diff line number Diff line change 6
6
7
7
\*******************************************************************/
8
8
9
-
10
9
#include " c_bit_field_replacement_type.h"
11
10
11
+ #include < util/invariant.h>
12
+
12
13
typet c_bit_field_replacement_type (
13
14
const c_bit_field_typet &src,
14
15
const namespacet &ns)
@@ -23,21 +24,18 @@ typet c_bit_field_replacement_type(
23
24
result.set_width (src.get_width ());
24
25
return std::move (result);
25
26
}
26
- else if (subtype. id ()==ID_c_enum_tag)
27
+ else
27
28
{
29
+ PRECONDITION (subtype.id () == ID_c_enum_tag);
30
+
28
31
const typet &sub_subtype=
29
32
ns.follow_tag (to_c_enum_tag_type (subtype)).subtype ();
30
33
31
- if (sub_subtype.id ()==ID_signedbv ||
32
- sub_subtype.id ()==ID_unsignedbv)
33
- {
34
- bitvector_typet result=to_bitvector_type (sub_subtype);
35
- result.set_width (src.get_width ());
36
- return std::move (result);
37
- }
38
- else
39
- return nil_typet ();
34
+ PRECONDITION (
35
+ sub_subtype.id () == ID_signedbv || sub_subtype.id () == ID_unsignedbv);
36
+
37
+ bitvector_typet result = to_bitvector_type (sub_subtype);
38
+ result.set_width (src.get_width ());
39
+ return std::move (result);
40
40
}
41
- else
42
- return nil_typet ();
43
41
}
You can’t perform that action at this time.
0 commit comments