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

Author: tautschnig

src/goto-instrument/dump_c.cpp

@@ -487,9 +487,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;

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(

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;

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;
     }

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

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

src/util/expr_initializer.cpp

@@ -188,20 +188,14 @@ optionalt<exprt> expr_initializert<nondet>::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;