File tree 7 files changed +40
-35
lines changed 7 files changed +40
-35
lines changed Original file line number Diff line number Diff line change @@ -532,9 +532,10 @@ void dump_ct::convert_compound(
532
532
{
533
533
const typet &comp_type = comp.type ();
534
534
535
- if (comp_type.id ()==ID_code ||
536
- comp.get_bool (ID_from_base) ||
537
- comp.get_is_padding ())
535
+ DATA_INVARIANT (
536
+ comp_type.id () != ID_code, " struct member must not be of code type" );
537
+
538
+ if (comp.get_bool (ID_from_base) || comp.get_is_padding ())
538
539
continue ;
539
540
540
541
const typet *non_array_type = &comp_type;
Original file line number Diff line number Diff line change @@ -147,10 +147,12 @@ std::string graphml_witnesst::convert_assign_rec(
147
147
assign.rhs ().operands ().begin ();
148
148
for (const auto &comp : components)
149
149
{
150
- if (comp.type ().id ()==ID_code ||
151
- comp.get_is_padding () ||
152
- // for some reason #is_padding gets lost in *some* cases
153
- has_prefix (id2string (comp.get_name ()), " $pad" ))
150
+ DATA_INVARIANT (
151
+ comp.type ().id () != ID_code, " struct member must not be of code type" );
152
+ if (
153
+ comp.get_is_padding () ||
154
+ // for some reason #is_padding gets lost in *some* cases
155
+ has_prefix (id2string (comp.get_name ()), " $pad" ))
154
156
continue ;
155
157
156
158
INVARIANT (
Original file line number Diff line number Diff line change @@ -976,10 +976,9 @@ mp_integer interpretert::get_size(const typet &type)
976
976
977
977
for (const auto &comp : components)
978
978
{
979
- const typet &sub_type=comp.type ();
980
-
981
- if (sub_type.id ()!=ID_code)
982
- sum+=get_size (sub_type);
979
+ DATA_INVARIANT (
980
+ comp.type ().id () != ID_code, " struct member must not be of code type" );
981
+ sum += get_size (comp.type ());
983
982
}
984
983
985
984
return sum;
@@ -993,10 +992,9 @@ mp_integer interpretert::get_size(const typet &type)
993
992
994
993
for (const auto &comp : components)
995
994
{
996
- const typet &sub_type=comp.type ();
997
-
998
- if (sub_type.id ()!=ID_code)
999
- max_size=std::max (max_size, get_size (sub_type));
995
+ DATA_INVARIANT (
996
+ comp.type ().id () != ID_code, " union member must not be of code type" );
997
+ max_size = std::max (max_size, get_size (comp.type ()));
1000
998
}
1001
999
1002
1000
return max_size;
Original file line number Diff line number Diff line change @@ -703,7 +703,10 @@ exprt gdb_value_extractort::get_struct_value(
703
703
{
704
704
const struct_typet::componentt &component = struct_type.components ()[i];
705
705
706
- if (component.get_is_padding () || component.type ().id () == ID_code)
706
+ DATA_INVARIANT (
707
+ component.type ().id () != ID_code,
708
+ " struct member must not be of code type" );
709
+ if (component.get_is_padding ())
707
710
{
708
711
continue ;
709
712
}
Original file line number Diff line number Diff line change @@ -1286,8 +1286,10 @@ void value_sett::assign(
1286
1286
const typet &subtype = c.type ();
1287
1287
const irep_idt &name = c.get_name ();
1288
1288
1289
- // ignore methods and padding
1290
- if (subtype.id () == ID_code || c.get_is_padding ())
1289
+ // ignore padding
1290
+ DATA_INVARIANT (
1291
+ subtype.id () != ID_code, " struct member must not be of code type" );
1292
+ if (c.get_is_padding ())
1291
1293
continue ;
1292
1294
1293
1295
member_exprt lhs_member (lhs, name, subtype);
@@ -1792,8 +1794,10 @@ void value_sett::erase_struct_union_symbol(
1792
1794
const typet &subtype = c.type ();
1793
1795
const irep_idt &name = c.get_name ();
1794
1796
1795
- // ignore methods and padding
1796
- if (subtype.id () == ID_code || c.get_is_padding ())
1797
+ // ignore padding
1798
+ DATA_INVARIANT (
1799
+ subtype.id () != ID_code, " struct/union member must not be of code type" );
1800
+ if (c.get_is_padding ())
1797
1801
continue ;
1798
1802
1799
1803
erase_symbol_rec (subtype, erase_prefix + " ." + id2string (name), ns);
Original file line number Diff line number Diff line change @@ -992,8 +992,11 @@ void value_set_fit::assign(
992
992
const typet &subtype=c_it->type ();
993
993
const irep_idt &name = c_it->get_name ();
994
994
995
- // ignore methods
996
- if (subtype.id ()==ID_code)
995
+ // ignore padding
996
+ DATA_INVARIANT (
997
+ subtype.id () != ID_code,
998
+ " struct/union member must not be of code type" );
999
+ if (c_it->get_is_padding ())
997
1000
continue ;
998
1001
999
1002
member_exprt lhs_member (lhs, name, subtype);
Original file line number Diff line number Diff line change @@ -188,20 +188,14 @@ optionalt<exprt> expr_initializert<nondet>::expr_initializer_rec(
188
188
189
189
for (const auto &c : components)
190
190
{
191
- if (c.type ().id () == ID_code)
192
- {
193
- constant_exprt code_value (ID_nil, c.type ());
194
- code_value.add_source_location ()=source_location;
195
- value.add_to_operands (std::move (code_value));
196
- }
197
- else
198
- {
199
- const auto member = expr_initializer_rec (c.type (), source_location);
200
- if (!member.has_value ())
201
- return {};
191
+ DATA_INVARIANT (
192
+ c.type ().id () != ID_code, " struct member must not be of code type" );
202
193
203
- value.add_to_operands (std::move (*member));
204
- }
194
+ const auto member = expr_initializer_rec (c.type (), source_location);
195
+ if (!member.has_value ())
196
+ return {};
197
+
198
+ value.add_to_operands (std::move (*member));
205
199
}
206
200
207
201
value.add_source_location ()=source_location;
You can’t perform that action at this time.
0 commit comments