Skip to content

Commit 356bcf4

Browse files
committed
GOTO programs do not have code-typed struct members
It's only the C++ front-end that puts methods in struct members, and this should not leak into GOTO programs. We can, therefore, clean up a number of unnecessary branches. Fixes: #6984
1 parent a930c37 commit 356bcf4

File tree

7 files changed

+40
-35
lines changed

7 files changed

+40
-35
lines changed

src/goto-instrument/dump_c.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff 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;

src/goto-programs/graphml_witness.cpp

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff 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(

src/goto-programs/interpreter.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff 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;

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff 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
}

src/pointer-analysis/value_set.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff 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);

src/pointer-analysis/value_set_fi.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff 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);

src/util/expr_initializer.cpp

Lines changed: 7 additions & 13 deletions
Original file line numberDiff line numberDiff 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;

0 commit comments

Comments
 (0)