Skip to content

Commit 646d5c0

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 cb36f17 commit 646d5c0

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
@@ -487,9 +487,10 @@ void dump_ct::convert_compound(
487487
{
488488
const typet &comp_type = comp.type();
489489

490-
if(comp_type.id()==ID_code ||
491-
comp.get_bool(ID_from_base) ||
492-
comp.get_is_padding())
490+
DATA_INVARIANT(
491+
comp_type.id() != ID_code, "struct member must not be of code type");
492+
493+
if(comp.get_bool(ID_from_base) || comp.get_is_padding())
493494
continue;
494495

495496
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
@@ -703,7 +703,10 @@ exprt gdb_value_extractort::get_struct_value(
703703
{
704704
const struct_typet::componentt &component = struct_type.components()[i];
705705

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())
707710
{
708711
continue;
709712
}

src/pointer-analysis/value_set.cpp

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1262,8 +1262,10 @@ void value_sett::assign(
12621262
const typet &subtype = c.type();
12631263
const irep_idt &name = c.get_name();
12641264

1265-
// ignore methods and padding
1266-
if(subtype.id() == ID_code || c.get_is_padding())
1265+
// ignore padding
1266+
DATA_INVARIANT(
1267+
subtype.id() != ID_code, "struct member must not be of code type");
1268+
if(c.get_is_padding())
12671269
continue;
12681270

12691271
member_exprt lhs_member(lhs, name, subtype);
@@ -1768,8 +1770,10 @@ void value_sett::erase_struct_union_symbol(
17681770
const typet &subtype = c.type();
17691771
const irep_idt &name = c.get_name();
17701772

1771-
// ignore methods and padding
1772-
if(subtype.id() == ID_code || c.get_is_padding())
1773+
// ignore padding
1774+
DATA_INVARIANT(
1775+
subtype.id() != ID_code, "struct/union member must not be of code type");
1776+
if(c.get_is_padding())
17731777
continue;
17741778

17751779
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
@@ -986,8 +986,11 @@ void value_set_fit::assign(
986986
const typet &subtype=c_it->type();
987987
const irep_idt &name = c_it->get_name();
988988

989-
// ignore methods
990-
if(subtype.id()==ID_code)
989+
// ignore padding
990+
DATA_INVARIANT(
991+
subtype.id() != ID_code,
992+
"struct/union member must not be of code type");
993+
if(c_it->get_is_padding())
991994
continue;
992995

993996
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)