File tree Expand file tree Collapse file tree 7 files changed +40
-35
lines changed Expand file tree Collapse file tree 7 files changed +40
-35
lines changed Original file line number Diff line number Diff line change @@ -486,9 +486,10 @@ void dump_ct::convert_compound(
486486 {
487487 const typet &comp_type = comp.type ();
488488
489- if (comp_type.id ()==ID_code ||
490- comp.get_bool (ID_from_base) ||
491- comp.get_is_padding ())
489+ DATA_INVARIANT (
490+ comp_type.id () != ID_code, " struct member must not be of code type" );
491+
492+ if (comp.get_bool (ID_from_base) || comp.get_is_padding ())
492493 continue ;
493494
494495 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(
147147 assign.rhs ().operands ().begin ();
148148 for (const auto &comp : components)
149149 {
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" ))
154156 continue ;
155157
156158 INVARIANT (
Original file line number Diff line number Diff line change @@ -976,10 +976,9 @@ mp_integer interpretert::get_size(const typet &type)
976976
977977 for (const auto &comp : components)
978978 {
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 ());
983982 }
984983
985984 return sum;
@@ -993,10 +992,9 @@ mp_integer interpretert::get_size(const typet &type)
993992
994993 for (const auto &comp : components)
995994 {
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 ()));
1000998 }
1001999
10021000 return max_size;
Original file line number Diff line number Diff line change @@ -702,7 +702,10 @@ exprt gdb_value_extractort::get_struct_value(
702702 {
703703 const struct_typet::componentt &component = struct_type.components ()[i];
704704
705- if (component.get_is_padding () || component.type ().id () == ID_code)
705+ DATA_INVARIANT (
706+ component.type ().id () != ID_code,
707+ " struct member must not be of code type" );
708+ if (component.get_is_padding ())
706709 {
707710 continue ;
708711 }
Original file line number Diff line number Diff line change @@ -1257,8 +1257,10 @@ void value_sett::assign(
12571257 const typet &subtype = c.type ();
12581258 const irep_idt &name = c.get_name ();
12591259
1260- // ignore methods and padding
1261- if (subtype.id () == ID_code || c.get_is_padding ())
1260+ // ignore padding
1261+ DATA_INVARIANT (
1262+ subtype.id () != ID_code, " struct member must not be of code type" );
1263+ if (c.get_is_padding ())
12621264 continue ;
12631265
12641266 member_exprt lhs_member (lhs, name, subtype);
@@ -1763,8 +1765,10 @@ void value_sett::erase_struct_union_symbol(
17631765 const typet &subtype = c.type ();
17641766 const irep_idt &name = c.get_name ();
17651767
1766- // ignore methods and padding
1767- if (subtype.id () == ID_code || c.get_is_padding ())
1768+ // ignore padding
1769+ DATA_INVARIANT (
1770+ subtype.id () != ID_code, " struct/union member must not be of code type" );
1771+ if (c.get_is_padding ())
17681772 continue ;
17691773
17701774 erase_symbol_rec (subtype, erase_prefix + " ." + id2string (name), ns);
Original file line number Diff line number Diff line change @@ -987,8 +987,11 @@ void value_set_fit::assign(
987987 const typet &subtype=c_it->type ();
988988 const irep_idt &name = c_it->get_name ();
989989
990- // ignore methods
991- if (subtype.id ()==ID_code)
990+ // ignore padding
991+ DATA_INVARIANT (
992+ subtype.id () != ID_code,
993+ " struct/union member must not be of code type" );
994+ if (c_it->get_is_padding ())
992995 continue ;
993996
994997 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(
188188
189189 for (const auto &c : components)
190190 {
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" );
202193
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));
205199 }
206200
207201 value.add_source_location ()=source_location;
You can’t perform that action at this time.
0 commit comments