Merge pull request #6892 from tautschnig/cleanup/no-code

GOTO programs do not have code-typed struct members

Author: tautschnig

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+40<dest.size())
-        {
-          sep=",\n    ";
-          last_size=dest.size();
-        }
-        else
-          sep=", ";
+        sep = ",\n    ";
+        last_size = dest.size();
       }
-
-      dest+=sep;
-      dest+='.';
-      irep_idt field_name = c.get_pretty_name();
-      if(field_name.empty())
-        field_name = c.get_name();
-      dest += id2string(field_name);
-      dest+='=';
-      dest+=tmp;
+      else
+        sep = ", ";
     }
 
+    dest += sep;
+    dest += '.';
+    irep_idt field_name = c.get_pretty_name();
+    if(field_name.empty())
+      field_name = c.get_name();
+    dest += id2string(field_name);
+    dest += '=';
+    dest += tmp;
+
     o_it++;
   }
 

src/ansi-c/c_typecheck_initializer.cpp

@@ -272,7 +272,10 @@ void c_typecheck_baset::designator_enter(
 
     for(const auto &c : struct_type.components())
     {
-      if(c.type().id() != ID_code && !c.get_is_padding())
+      DATA_INVARIANT(
+        c.type().id() != ID_code, "struct member must not be of code type");
+
+      if(!c.get_is_padding())
       {
         entry.subtype = c.type();
         break;
@@ -457,9 +460,12 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
       DATA_INVARIANT(index<components.size(),
                      "member designator is bounded by components size");
-      DATA_INVARIANT(components[index].type().id()!=ID_code &&
-                     !components[index].get_is_padding(),
-                     "member designator points at data member");
+      DATA_INVARIANT(
+        components[index].type().id() != ID_code,
+        "struct member must not be of code type");
+      DATA_INVARIANT(
+        !components[index].get_is_padding(),
+        "member designator points at non-padding member");
 
       dest=&(dest->operands()[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++;
       }

src/ansi-c/expr2c.cpp

@@ -2078,8 +2078,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)
     {

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;

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;