diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp index bff889ab712..7c5414bf402 100644 --- a/jbmc/src/java_bytecode/expr2java.cpp +++ b/jbmc/src/java_bytecode/expr2java.cpp @@ -126,34 +126,34 @@ std::string expr2javat::convert_struct( for(const auto &c : components) { - if(c.type().id() != ID_code) - { - std::string tmp=convert(*o_it); - std::string sep; + DATA_INVARIANT( + c.type().id() != ID_code, "struct member must not be of code type"); - if(first) - first=false; - else + std::string tmp = convert(*o_it); + std::string sep; + + if(first) + first = false; + else + { + if(last_size + 40 < dest.size()) { - if(last_size+40operands()[index]); } @@ -737,8 +743,7 @@ void c_typecheck_baset::increment_designator(designatort &designator) (components[entry.index].get_is_padding() || (components[entry.index].get_anonymous() && components[entry.index].type().id() != ID_struct_tag && - components[entry.index].type().id() != ID_union_tag) || - components[entry.index].type().id() == ID_code)) + components[entry.index].type().id() != ID_union_tag))) { entry.index++; } diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index d1e94046fef..53c2fc52b63 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -2074,8 +2074,8 @@ std::string expr2ct::convert_struct( for(const auto &component : struct_type.components()) { - if(o_it->type().id()==ID_code) - continue; + DATA_INVARIANT( + o_it->type().id() != ID_code, "struct member must not be of code type"); if(component.get_is_padding() && !include_padding_components) { diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 06b3e22ca8f..1c5f7f61d0e 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -532,9 +532,10 @@ void dump_ct::convert_compound( { const typet &comp_type = comp.type(); - if(comp_type.id()==ID_code || - comp.get_bool(ID_from_base) || - comp.get_is_padding()) + DATA_INVARIANT( + comp_type.id() != ID_code, "struct member must not be of code type"); + + if(comp.get_bool(ID_from_base) || comp.get_is_padding()) continue; const typet *non_array_type = &comp_type; diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp index b83e192ef0c..5d1558b0a57 100644 --- a/src/goto-programs/graphml_witness.cpp +++ b/src/goto-programs/graphml_witness.cpp @@ -147,10 +147,12 @@ std::string graphml_witnesst::convert_assign_rec( assign.rhs().operands().begin(); for(const auto &comp : components) { - if(comp.type().id()==ID_code || - comp.get_is_padding() || - // for some reason #is_padding gets lost in *some* cases - has_prefix(id2string(comp.get_name()), "$pad")) + DATA_INVARIANT( + comp.type().id() != ID_code, "struct member must not be of code type"); + if( + comp.get_is_padding() || + // for some reason #is_padding gets lost in *some* cases + has_prefix(id2string(comp.get_name()), "$pad")) continue; INVARIANT( diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index 155311a205e..d3572e6954a 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -976,10 +976,9 @@ mp_integer interpretert::get_size(const typet &type) for(const auto &comp : components) { - const typet &sub_type=comp.type(); - - if(sub_type.id()!=ID_code) - sum+=get_size(sub_type); + DATA_INVARIANT( + comp.type().id() != ID_code, "struct member must not be of code type"); + sum += get_size(comp.type()); } return sum; @@ -993,10 +992,9 @@ mp_integer interpretert::get_size(const typet &type) for(const auto &comp : components) { - const typet &sub_type=comp.type(); - - if(sub_type.id()!=ID_code) - max_size=std::max(max_size, get_size(sub_type)); + DATA_INVARIANT( + comp.type().id() != ID_code, "union member must not be of code type"); + max_size = std::max(max_size, get_size(comp.type())); } return max_size; diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index b1361497555..b7f9c9c9da3 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -703,7 +703,10 @@ exprt gdb_value_extractort::get_struct_value( { const struct_typet::componentt &component = struct_type.components()[i]; - if(component.get_is_padding() || component.type().id() == ID_code) + DATA_INVARIANT( + component.type().id() != ID_code, + "struct member must not be of code type"); + if(component.get_is_padding()) { continue; } diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 379b0adf8ea..f3f1fa99084 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1286,8 +1286,10 @@ void value_sett::assign( const typet &subtype = c.type(); const irep_idt &name = c.get_name(); - // ignore methods and padding - if(subtype.id() == ID_code || c.get_is_padding()) + // ignore padding + DATA_INVARIANT( + subtype.id() != ID_code, "struct member must not be of code type"); + if(c.get_is_padding()) continue; member_exprt lhs_member(lhs, name, subtype); @@ -1792,8 +1794,10 @@ void value_sett::erase_struct_union_symbol( const typet &subtype = c.type(); const irep_idt &name = c.get_name(); - // ignore methods and padding - if(subtype.id() == ID_code || c.get_is_padding()) + // ignore padding + DATA_INVARIANT( + subtype.id() != ID_code, "struct/union member must not be of code type"); + if(c.get_is_padding()) continue; erase_symbol_rec(subtype, erase_prefix + "." + id2string(name), ns); diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index f86582ac8b8..fdf9998e791 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -992,8 +992,11 @@ void value_set_fit::assign( const typet &subtype=c_it->type(); const irep_idt &name = c_it->get_name(); - // ignore methods - if(subtype.id()==ID_code) + // ignore padding + DATA_INVARIANT( + subtype.id() != ID_code, + "struct/union member must not be of code type"); + if(c_it->get_is_padding()) continue; member_exprt lhs_member(lhs, name, subtype); diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index cc24fe0ce88..fb8808887b9 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -188,20 +188,14 @@ optionalt expr_initializert::expr_initializer_rec( for(const auto &c : components) { - if(c.type().id() == ID_code) - { - constant_exprt code_value(ID_nil, c.type()); - code_value.add_source_location()=source_location; - value.add_to_operands(std::move(code_value)); - } - else - { - const auto member = expr_initializer_rec(c.type(), source_location); - if(!member.has_value()) - return {}; + DATA_INVARIANT( + c.type().id() != ID_code, "struct member must not be of code type"); - value.add_to_operands(std::move(*member)); - } + const auto member = expr_initializer_rec(c.type(), source_location); + if(!member.has_value()) + return {}; + + value.add_to_operands(std::move(*member)); } value.add_source_location()=source_location;